Commit 2023-02-11 07:51 ddd9ba0b

View on Github →

feat: port Topology.DiscreteQuotient (#2157) Also sync SHA in Topology.Connected. The changes in Mathlib 3 were backported from this branch, see

topology.connected@92ca63f0fb391a9ca5f22d2409a6080e786d99f7..d101e93197bb5f6ea89bd7ba386b7f7dff1f3903

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Connected.lean

added theorem connectedComponent_eq_iff_mem

added theorem connectedComponent_eq_singleton

Created Mathlib/Topology/DiscreteQuotient.lean

added theorem DiscreteQuotient.LeComap.comp

added theorem DiscreteQuotient.LeComap.mono

added def DiscreteQuotient.LeComap

added def DiscreteQuotient.comap

added theorem DiscreteQuotient.comap_comp

added theorem DiscreteQuotient.comap_id

added theorem DiscreteQuotient.comap_mono

added theorem DiscreteQuotient.eq_of_forall_proj_eq

added theorem DiscreteQuotient.exists_of_compat

added theorem DiscreteQuotient.fiber_eq

added theorem DiscreteQuotient.fiber_subset_ofLe

added theorem DiscreteQuotient.isClopen_preimage

added theorem DiscreteQuotient.isClopen_setOf_rel

added theorem DiscreteQuotient.isClosed_preimage

added theorem DiscreteQuotient.isOpen_preimage

added theorem DiscreteQuotient.leComap_id

added theorem DiscreteQuotient.leComap_id_iff

added def DiscreteQuotient.map

added theorem DiscreteQuotient.map_comp

added theorem DiscreteQuotient.map_comp_ofLe

added theorem DiscreteQuotient.map_comp_proj

added theorem DiscreteQuotient.map_continuous

added theorem DiscreteQuotient.map_id

added theorem DiscreteQuotient.map_ofLe

added theorem DiscreteQuotient.map_proj

added def DiscreteQuotient.ofClopen

added def DiscreteQuotient.ofLe

added theorem DiscreteQuotient.ofLe_comp_map

added theorem DiscreteQuotient.ofLe_comp_ofLe

added theorem DiscreteQuotient.ofLe_comp_proj

added theorem DiscreteQuotient.ofLe_continuous

added theorem DiscreteQuotient.ofLe_map

added theorem DiscreteQuotient.ofLe_ofLe

added theorem DiscreteQuotient.ofLe_proj

added theorem DiscreteQuotient.ofLe_refl

added theorem DiscreteQuotient.ofLe_refl_apply

added def DiscreteQuotient.proj

added theorem DiscreteQuotient.proj_bot_bijective

added theorem DiscreteQuotient.proj_bot_eq

added theorem DiscreteQuotient.proj_bot_inj

added theorem DiscreteQuotient.proj_bot_injective

added theorem DiscreteQuotient.proj_continuous

added theorem DiscreteQuotient.proj_isLocallyConstant

added theorem DiscreteQuotient.proj_quotientMap

added theorem DiscreteQuotient.proj_surjective

added theorem DiscreteQuotient.refl

added theorem DiscreteQuotient.symm

added theorem DiscreteQuotient.toSetoid_injective

added theorem DiscreteQuotient.trans

added structure DiscreteQuotient

added def LocallyConstant.discreteQuotient

added def LocallyConstant.lift

added theorem LocallyConstant.lift_comp_proj