DiscreteQuotient

📁 Source: Mathlib/Topology/DiscreteQuotient.lean

Statistics

Metric	Count
Definitions `DiscreteQuotient`, `LEComap`, `comap`, `equivFinsetClopens`, `finsetClopens`, `inhabitedQuotient`, `instCoeSortType`, `instInhabited`, `instMin`, `instOrderBotOfLocallyConnectedSpace`, `instOrderTop`, `instPartialOrder`, `instSemilatticeInf`, `instTopologicalSpaceQuotient`, `map`, `ofIsClopen`, `ofLE`, `proj`, `toSetoid`, `discreteQuotient`	20
Theorems `comp`, `mono`, `comap_comp`, `comap_id`, `comap_mono`, `comp_finsetClopens`, `eq_of_forall_proj_eq`, `exists_of_compat`, `ext`, `ext_iff`, `fiber_eq`, `fiber_subset_ofLE`, `finsetClopens_inj`, `instDiscreteTopologyQuotient`, `instFiniteQuotientOfCompactSpace`, `instNonemptyQuotient`, `instSubsingletonQuotientTop`, `isClopen_preimage`, `isClopen_setOf_rel`, `isClosed_preimage`, `isOpen_preimage`, `isOpen_setOf_rel`, `leComap_id`, `leComap_id_iff`, `map_comp`, `map_comp_ofLE`, `map_comp_proj`, `map_continuous`, `map_id`, `map_ofLE`, `map_proj`, `ofLE_comp_map`, `ofLE_comp_ofLE`, `ofLE_comp_proj`, `ofLE_continuous`, `ofLE_map`, `ofLE_ofLE`, `ofLE_proj`, `ofLE_refl`, `ofLE_refl_apply`, `proj_bot_bijective`, `proj_bot_eq`, `proj_bot_inj`, `proj_bot_injective`, `proj_continuous`, `proj_isLocallyConstant`, `proj_isQuotientMap`, `proj_surjective`, `refl`, `toSetoid_injective`, `trans`, `lift_comp_proj`	52
Total	72

DiscreteQuotient

Definitions

Name	Category	Theorems
`LEComap` 📖	MathDef	2 math math: `leComap_id`, `leComap_id_iff`
`comap` 📖	CompOp	3 math math: `comap_mono`, `comap_comp`, `comap_id`
`equivFinsetClopens` 📖	CompOp	—
`finsetClopens` 📖	CompOp	2 math math: `finsetClopens_inj`, `comp_finsetClopens`
`inhabitedQuotient` 📖	CompOp	—
`instCoeSortType` 📖	CompOp	—
`instInhabited` 📖	CompOp	—
`instMin` 📖	CompOp	—
`instOrderBotOfLocallyConnectedSpace` 📖	CompOp	4 math math: `proj_bot_inj`, `proj_bot_bijective`, `proj_bot_eq`, `proj_bot_injective`
`instOrderTop` 📖	CompOp	1 math math: `instSubsingletonQuotientTop`
`instPartialOrder` 📖	CompOp	13 math math: `ofLE_refl`, `proj_bot_inj`, `LightProfinite.lightToProfinite_map_proj_eq`, `proj_bot_bijective`, `Profinite.instEpiAppDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceπAsLimitCone`, `leComap_id_iff`, `Condensed.instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp`, `Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply`, `instSubsingletonQuotientTop`, `proj_bot_eq`, `ofLE_refl_apply`, `Profinite.isIso_asLimitCone_lift`, `proj_bot_injective`
`instSemilatticeInf` 📖	CompOp	—
`instTopologicalSpaceQuotient` 📖	CompOp	6 math math: `ofLE_continuous`, `proj_continuous`, `instDiscreteTopologyQuotient`, `proj_isQuotientMap`, `LocallyConstant.lift_comp_proj`, `map_continuous`
`map` 📖	CompOp	9 math math: `map_id`, `map_comp_proj`, `ofLE_map`, `map_comp_ofLE`, `map_ofLE`, `map_comp`, `map_continuous`, `ofLE_comp_map`, `map_proj`
`ofIsClopen` 📖	CompOp	—
`ofLE` 📖	CompOp	12 math math: `ofLE_proj`, `ofLE_refl`, `fiber_subset_ofLE`, `ofLE_continuous`, `ofLE_map`, `ofLE_ofLE`, `ofLE_comp_ofLE`, `ofLE_comp_proj`, `map_comp_ofLE`, `ofLE_refl_apply`, `map_ofLE`, `ofLE_comp_map`
`proj` 📖	CompOp	19 math math: `ofLE_proj`, `proj_bot_inj`, `fiber_subset_ofLE`, `map_comp_proj`, `proj_continuous`, `fiber_eq`, `proj_bot_bijective`, `isClopen_preimage`, `ofLE_comp_proj`, `isClosed_preimage`, `proj_isQuotientMap`, `exists_of_compat`, `proj_bot_eq`, `proj_isLocallyConstant`, `proj_surjective`, `LocallyConstant.lift_comp_proj`, `isOpen_preimage`, `proj_bot_injective`, `map_proj`
`toSetoid` 📖	CompOp	31 math math: `ofLE_refl`, `map_id`, `fiber_subset_ofLE`, `ofLE_continuous`, `isOpen_setOf_rel`, `map_comp_proj`, `proj_continuous`, `fiber_eq`, `proj_bot_bijective`, `isClopen_preimage`, `ext_iff`, `ofLE_comp_ofLE`, `toSetoid_injective`, `instDiscreteTopologyQuotient`, `instFiniteQuotientOfCompactSpace`, `ofLE_comp_proj`, `isClosed_preimage`, `map_comp_ofLE`, `proj_isQuotientMap`, `instNonemptyQuotient`, `instSubsingletonQuotientTop`, `isClopen_setOf_rel`, `proj_isLocallyConstant`, `proj_surjective`, `LocallyConstant.lift_comp_proj`, `refl`, `isOpen_preimage`, `map_comp`, `map_continuous`, `proj_bot_injective`, `ofLE_comp_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_comp` 📖	mathematical	—	`comap` `ContinuousMap.comp`	—	—
`comap_id` 📖	mathematical	—	`comap` `ContinuousMap.id`	—	—
`comap_mono` 📖	mathematical	`DiscreteQuotient` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`comap`	—	—
`comp_finsetClopens` 📖	mathematical	—	`DiscreteQuotient` `Finset` `TopologicalSpace.Clopens` `Set` `Set.image` `TopologicalSpace.Clopens.carrier` `SetLike.coe` `Finset.instSetLike` `finsetClopens` `Setoid.classes`	—	`Set.ext` `instFiniteQuotientOfCompactSpace` `Set.coe_toFinset` `Quotient.mk_eq_iff_out`
`eq_of_forall_proj_eq` 📖	—	`proj`	—	—	`Set.mem_singleton_iff` `connectedComponent_eq_singleton` `connectedComponent_eq_iInter_isClopen` `Set.mem_iInter` `Quotient.exact'`
`exists_of_compat` 📖	mathematical	`ofLE`	`proj`	—	`fiber_subset_ofLE` `IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed` `directed_of_isDirected_ge` `SemilatticeInf.instIsCodirectedOrder` `Set.Nonempty.preimage` `Set.singleton_nonempty` `proj_surjective` `IsClosed.isCompact` `isClosed_preimage` `Set.mem_iInter`
`ext` 📖	—	`toSetoid`	—	—	—
`ext_iff` 📖	mathematical	—	`toSetoid`	—	`ext`
`fiber_eq` 📖	mathematical	—	`Set.preimage` `toSetoid` `proj` `Set` `Set.instSingletonSet` `setOf`	—	`Set.ext` `Quotient.eq''`
`fiber_subset_ofLE` 📖	mathematical	`DiscreteQuotient` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Set` `Set.instHasSubset` `Set.preimage` `toSetoid` `proj` `Set.instSingletonSet` `ofLE`	—	`proj_surjective` `fiber_eq` `ofLE_proj`
`finsetClopens_inj` 📖	mathematical	—	`DiscreteQuotient` `Finset` `TopologicalSpace.Clopens` `finsetClopens`	—	`Function.Injective.of_comp` `comp_finsetClopens`
`instDiscreteTopologyQuotient` 📖	mathematical	—	`DiscreteTopology` `toSetoid` `instTopologicalSpaceQuotient`	—	`discreteTopology_iff_isOpen_singleton` `Function.Surjective.forall` `proj_surjective` `Topology.IsQuotientMap.isOpen_preimage` `proj_isQuotientMap` `fiber_eq` `isOpen_setOf_rel`
`instFiniteQuotientOfCompactSpace` 📖	mathematical	—	`Finite` `toSetoid`	—	`Quotient.compactSpace` `Set.finite_univ_iff` `isCompact_iff_finite` `instDiscreteTopologyQuotient` `isCompact_univ_iff`
`instNonemptyQuotient` 📖	mathematical	—	`toSetoid`	—	`Nonempty.map`
`instSubsingletonQuotientTop` 📖	mathematical	—	`toSetoid` `Top.top` `DiscreteQuotient` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOrderTop`	—	—
`isClopen_preimage` 📖	mathematical	—	`IsClopen` `Set.preimage` `toSetoid` `proj`	—	`IsClopen.preimage` `isClopen_discrete` `instDiscreteTopologyQuotient` `proj_continuous`
`isClopen_setOf_rel` 📖	mathematical	—	`IsClopen` `setOf` `toSetoid`	—	`fiber_eq` `isClopen_preimage`
`isClosed_preimage` 📖	mathematical	—	`IsClosed` `Set.preimage` `toSetoid` `proj`	—	`isClopen_preimage`
`isOpen_preimage` 📖	mathematical	—	`IsOpen` `Set.preimage` `toSetoid` `proj`	—	`isClopen_preimage`
`isOpen_setOf_rel` 📖	mathematical	—	`IsOpen` `setOf` `toSetoid`	—	—
`leComap_id` 📖	mathematical	—	`LEComap` `ContinuousMap.id`	—	`le_rfl`
`leComap_id_iff` 📖	mathematical	—	`LEComap` `ContinuousMap.id` `DiscreteQuotient` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	—	—
`map_comp` 📖	mathematical	`LEComap`	`map` `ContinuousMap.comp` `LEComap.comp` `toSetoid`	—	`LEComap.comp`
`map_comp_ofLE` 📖	mathematical	`LEComap` `DiscreteQuotient` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`toSetoid` `map` `ofLE` `LEComap.mono` `le_rfl`	—	`LEComap.mono` `le_rfl` `map_ofLE`
`map_comp_proj` 📖	mathematical	`LEComap`	`toSetoid` `map` `proj` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	—	—
`map_continuous` 📖	mathematical	`LEComap`	`Continuous` `toSetoid` `instTopologicalSpaceQuotient` `map`	—	`continuous_of_discreteTopology` `instDiscreteTopologyQuotient`
`map_id` 📖	mathematical	—	`map` `ContinuousMap.id` `leComap_id` `toSetoid`	—	`leComap_id`
`map_ofLE` 📖	mathematical	`LEComap` `DiscreteQuotient` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`map` `ofLE` `LEComap.mono` `le_rfl`	—	`LEComap.mono` `le_rfl`
`map_proj` 📖	mathematical	`LEComap`	`map` `proj` `DFunLike.coe` `ContinuousMap` `ContinuousMap.instFunLike`	—	—
`ofLE_comp_map` 📖	mathematical	`LEComap` `DiscreteQuotient` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`toSetoid` `ofLE` `map` `LEComap.mono` `le_rfl`	—	`LEComap.mono` `le_rfl` `ofLE_map`
`ofLE_comp_ofLE` 📖	mathematical	`DiscreteQuotient` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`toSetoid` `ofLE` `le_trans`	—	`le_trans` `ofLE_ofLE`
`ofLE_comp_proj` 📖	mathematical	`DiscreteQuotient` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`toSetoid` `ofLE` `proj`	—	`ofLE_proj`
`ofLE_continuous` 📖	mathematical	`DiscreteQuotient` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Continuous` `toSetoid` `instTopologicalSpaceQuotient` `ofLE`	—	`continuous_of_discreteTopology` `instDiscreteTopologyQuotient`
`ofLE_map` 📖	mathematical	`LEComap` `DiscreteQuotient` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`ofLE` `map` `LEComap.mono` `le_rfl`	—	`LEComap.mono` `le_rfl`
`ofLE_ofLE` 📖	mathematical	`DiscreteQuotient` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`ofLE` `LE.le.trans`	—	`LE.le.trans`
`ofLE_proj` 📖	mathematical	`DiscreteQuotient` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`ofLE` `proj`	—	`Quotient.sound'` `refl`
`ofLE_refl` 📖	mathematical	—	`ofLE` `le_refl` `DiscreteQuotient` `PartialOrder.toPreorder` `instPartialOrder` `toSetoid`	—	`le_refl`
`ofLE_refl_apply` 📖	mathematical	—	`ofLE` `le_refl` `DiscreteQuotient` `PartialOrder.toPreorder` `instPartialOrder`	—	`le_refl` `ofLE_refl`
`proj_bot_bijective` 📖	mathematical	—	`Function.Bijective` `toSetoid` `Bot.bot` `DiscreteQuotient` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOrderBotOfLocallyConnectedSpace` `DiscreteTopology.toLocallyConnectedSpace` `proj`	—	`DiscreteTopology.toLocallyConnectedSpace` `proj_bot_injective` `proj_surjective`
`proj_bot_eq` 📖	mathematical	—	`proj` `Bot.bot` `DiscreteQuotient` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOrderBotOfLocallyConnectedSpace` `connectedComponent`	—	`Quotient.eq''`
`proj_bot_inj` 📖	mathematical	—	`proj` `Bot.bot` `DiscreteQuotient` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOrderBotOfLocallyConnectedSpace` `DiscreteTopology.toLocallyConnectedSpace`	—	`DiscreteTopology.toLocallyConnectedSpace` `connectedComponent_eq_singleton` `TotallySeparatedSpace.totallyDisconnectedSpace` `TotallySeparatedSpace.of_discrete`
`proj_bot_injective` 📖	mathematical	—	`toSetoid` `Bot.bot` `DiscreteQuotient` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `instOrderBotOfLocallyConnectedSpace` `DiscreteTopology.toLocallyConnectedSpace` `proj`	—	`DiscreteTopology.toLocallyConnectedSpace`
`proj_continuous` 📖	mathematical	—	`Continuous` `toSetoid` `instTopologicalSpaceQuotient` `proj`	—	`Topology.IsQuotientMap.continuous` `proj_isQuotientMap`
`proj_isLocallyConstant` 📖	mathematical	—	`IsLocallyConstant` `toSetoid` `proj`	—	`IsLocallyConstant.iff_continuous` `instDiscreteTopologyQuotient` `proj_continuous`
`proj_isQuotientMap` 📖	mathematical	—	`Topology.IsQuotientMap` `toSetoid` `instTopologicalSpaceQuotient` `proj`	—	—
`proj_surjective` 📖	mathematical	—	`toSetoid` `proj`	—	`Quotient.mk''_surjective`
`refl` 📖	mathematical	—	`toSetoid`	—	`Setoid.refl'`
`toSetoid_injective` 📖	mathematical	—	`DiscreteQuotient` `toSetoid`	—	—
`trans` 📖	—	`toSetoid`	—	—	`Setoid.trans'`

DiscreteQuotient.LEComap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp` 📖	mathematical	`DiscreteQuotient.LEComap`	`ContinuousMap.comp`	—	—
`mono` 📖	—	`DiscreteQuotient.LEComap` `DiscreteQuotient` `Preorder.toLE` `PartialOrder.toPreorder` `DiscreteQuotient.instPartialOrder`	—	—	`LE.le.trans` `DiscreteQuotient.comap_mono`

LocallyConstant

Definitions

Name	Category	Theorems
`discreteQuotient` 📖	CompOp	1 math math: `lift_comp_proj`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lift_comp_proj` 📖	mathematical	—	`DiscreteQuotient.toSetoid` `discreteQuotient` `DFunLike.coe` `LocallyConstant` `DiscreteQuotient.instTopologicalSpaceQuotient` `instFunLike` `lift` `DiscreteQuotient.proj`	—	—

(root)

Definitions

Name	Category	Theorems
`DiscreteQuotient` 📖	CompData	17 math math: `DiscreteQuotient.ofLE_refl`, `DiscreteQuotient.proj_bot_inj`, `DiscreteQuotient.finsetClopens_inj`, `LightProfinite.lightToProfinite_map_proj_eq`, `DiscreteQuotient.proj_bot_bijective`, `LightProfinite.instCountableDiscreteQuotient`, `Profinite.instEpiAppDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceπAsLimitCone`, `DiscreteQuotient.leComap_id_iff`, `DiscreteQuotient.comp_finsetClopens`, `Condensed.instFinalOppositeDiscreteQuotientCarrierToTopTotallyDisconnectedSpaceCostructuredArrowFintypeCatProfiniteOpToProfiniteOpPtAsLimitConeFunctorOp`, `DiscreteQuotient.toSetoid_injective`, `Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply`, `DiscreteQuotient.instSubsingletonQuotientTop`, `DiscreteQuotient.proj_bot_eq`, `DiscreteQuotient.ofLE_refl_apply`, `Profinite.isIso_asLimitCone_lift`, `DiscreteQuotient.proj_bot_injective`

---

← Back to Index