Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-08 18:27 d101e931

View on Github →

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 setoids;
  • 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.

Estimated changes

modified theorem discrete_quotient.comap_id
modified def discrete_quotient.map
modified theorem discrete_quotient.map_comp
modified theorem discrete_quotient.map_id
modified theorem discrete_quotient.map_of_le
modified theorem discrete_quotient.map_proj
modified theorem discrete_quotient.of_le_map
modified theorem discrete_quotient.refl
modified theorem discrete_quotient.symm
modified theorem discrete_quotient.trans
modified structure discrete_quotient