Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
refactor(topology/discrete_quotient): review API (#18401)
Backport various changes I made to the API while porting to Lean 4 in leanprover-community/mathlib4#2157. * extend `setoid X`; * require only that the fibers are open in the definition, prove that they are clopen; * golf proofs, reuse lattice structure on `setoid`s; * use bundled continuous maps for `comap`; * swap LHS and RHS in some `simp` lemmas; * generalize the `order_bot` instance from a discrete space to a locally connected space; * prove that a discrete topological space is locally connected.
- Loading branch information
Showing
3 changed files
with
179 additions
and
197 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.