This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 387ff6e

shingtaklam1324

committed

feat(topology/homotopy): add homotopy_with (#9252)

Added `homotopy_with` as in [`HOL-Analysis`](https://isabelle.in.tum.de/library/HOL/HOL-Analysis/Homotopy.html) extending `homotopy`. Furthermore, I've added `homotopy_rel`. Also rename/moved the file. There is also some refactoring which is part of the suggestions from #9141 .

1 parent f6c77be commit 387ff6eCopy full SHA for 387ff6e

2 files changed

+418

-190

lines changed

src/topology
- homotopy.lean
- homotopy
  - basic.lean

2 files changed

+418

-190

lines changed

`‎src/topology/homotopy.lean`

This file was deleted.

Comments

(0)