Commit 2023-02-08 18:27 d101e931

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.