StoneCech

📁 Source: Mathlib/Topology/Compactification/StoneCech.lean

Statistics

Metric	Count
Definitions `PreStoneCech`, `StoneCech`, `extend`, `topologicalSpace`, `instInhabitedPreStoneCech`, `instInhabitedStoneCech`, `instTopologicalSpacePreStoneCech`, `instTopologicalSpaceStoneCech`, `preStoneCechExtend`, `preStoneCechUnit`, `stoneCechExtend`, `stoneCechUnit`, `ultrafilterBasis`	13
Theorems `t2Space`, `tendsto_pure_self`, `continuous_preStoneCechExtend`, `continuous_preStoneCechUnit`, `continuous_stoneCechExtend`, `continuous_stoneCechUnit`, `continuous_ultrafilter_extend`, `denseRange_preStoneCechUnit`, `denseRange_pure`, `denseRange_stoneCechUnit`, `eq_if_preStoneCechUnit_eq`, `eq_if_stoneCechUnit_eq`, `induced_topology_pure`, `instCompactSpacePreStoneCech`, `instCompactSpaceStoneCech`, `instT2SpaceStoneCech`, `instTotallyDisconnectedSpaceUltrafilter`, `isDenseEmbedding_pure`, `isDenseInducing_pure`, `preStoneCechCompat`, `preStoneCechExtend_extends`, `preStoneCechExtend_preStoneCechUnit`, `preStoneCech_hom_ext`, `stoneCechExtend_extends`, `stoneCechExtend_stoneCechUnit`, `stoneCech_hom_ext`, `ultrafilterBasis_is_basis`, `ultrafilter_comap_pure_nhds`, `ultrafilter_compact`, `ultrafilter_converges_iff`, `ultrafilter_extend_eq_iff`, `ultrafilter_extend_extends`, `ultrafilter_extend_pure`, `ultrafilter_isClosed_basic`, `ultrafilter_isOpen_basic`	35
Total	48

Ultrafilter

Definitions

Name	Category	Theorems
`extend` 📖	CompOp	5 math math: `ultrafilter_extend_extends`, `continuous_ultrafilter_extend`, `ultrafilter_extend_eq_iff`, `preStoneCechCompat`, `ultrafilter_extend_pure`
`topologicalSpace` 📖	CompOp	19 math math: `ultrafilter_compact`, `denseRange_pure`, `induced_topology_pure`, `isDenseEmbedding_pure`, `continuous_add_left`, `ultrafilterBasis_is_basis`, `Profinite.projective_ultrafilter`, `instTotallyDisconnectedSpaceUltrafilter`, `isProperMap_iff_isClosedMap_ultrafilter`, `ultrafilter_isOpen_basic`, `isDenseInducing_pure`, `tendsto_pure_self`, `t2Space`, `continuous_ultrafilter_extend`, `CompHaus.projective_ultrafilter`, `ultrafilter_isClosed_basic`, `ultrafilter_converges_iff`, `ultrafilter_comap_pure_nhds`, `continuous_mul_left`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`t2Space` 📖	mathematical	—	`T2Space` `Ultrafilter` `topologicalSpace`	—	`t2_iff_ultrafilter` `ultrafilter_converges_iff`
`tendsto_pure_self` 📖	mathematical	—	`Filter.Tendsto` `Ultrafilter` `instPure` `toFilter` `nhds` `topologicalSpace`	—	`Filter.Tendsto.eq_1` `coe_map` `ultrafilter_converges_iff` `ext`

(root)

Definitions

Name	Category	Theorems
`PreStoneCech` 📖	CompOp	5 math math: `continuous_preStoneCechExtend`, `denseRange_preStoneCechUnit`, `preStoneCechExtend_extends`, `continuous_preStoneCechUnit`, `instCompactSpacePreStoneCech`
`StoneCech` 📖	CompOp	16 math math: `continuous_stoneCechUnit`, `instCompactSpaceStoneCech`, `isDenseEmbedding_stoneCechUnit`, `instT2SpaceStoneCech`, `isDenseInducing_stoneCechUnit`, `isInducing_stoneCechUnit`, `t35Space_iff_isEmbedding_stoneCechUnit`, `isEmbedding_stoneCechUnit`, `StoneCech.projective`, `continuous_stoneCechExtend`, `stoneCechObj_toTop_carrier`, `stoneCechExtend_extends`, `denseRange_stoneCechUnit`, `completelyRegularSpace_iff_isInducing_stoneCechUnit`, `injective_stoneCechUnit_of_t35Space`, `topToCompHaus_obj`
`instInhabitedPreStoneCech` 📖	CompOp	—
`instInhabitedStoneCech` 📖	CompOp	—
`instTopologicalSpacePreStoneCech` 📖	CompOp	4 math math: `continuous_preStoneCechExtend`, `denseRange_preStoneCechUnit`, `continuous_preStoneCechUnit`, `instCompactSpacePreStoneCech`
`instTopologicalSpaceStoneCech` 📖	CompOp	12 math math: `continuous_stoneCechUnit`, `instCompactSpaceStoneCech`, `isDenseEmbedding_stoneCechUnit`, `instT2SpaceStoneCech`, `isDenseInducing_stoneCechUnit`, `isInducing_stoneCechUnit`, `t35Space_iff_isEmbedding_stoneCechUnit`, `isEmbedding_stoneCechUnit`, `StoneCech.projective`, `continuous_stoneCechExtend`, `denseRange_stoneCechUnit`, `completelyRegularSpace_iff_isInducing_stoneCechUnit`
`preStoneCechExtend` 📖	CompOp	3 math math: `continuous_preStoneCechExtend`, `preStoneCechExtend_preStoneCechUnit`, `preStoneCechExtend_extends`
`preStoneCechUnit` 📖	CompOp	4 math math: `denseRange_preStoneCechUnit`, `preStoneCechExtend_preStoneCechUnit`, `preStoneCechExtend_extends`, `continuous_preStoneCechUnit`
`stoneCechExtend` 📖	CompOp	3 math math: `continuous_stoneCechExtend`, `stoneCechExtend_extends`, `stoneCechExtend_stoneCechUnit`
`stoneCechUnit` 📖	CompOp	11 math math: `continuous_stoneCechUnit`, `isDenseEmbedding_stoneCechUnit`, `isDenseInducing_stoneCechUnit`, `isInducing_stoneCechUnit`, `t35Space_iff_isEmbedding_stoneCechUnit`, `isEmbedding_stoneCechUnit`, `stoneCechExtend_extends`, `denseRange_stoneCechUnit`, `completelyRegularSpace_iff_isInducing_stoneCechUnit`, `stoneCechExtend_stoneCechUnit`, `injective_stoneCechUnit_of_t35Space`
`ultrafilterBasis` 📖	CompOp	1 math math: `ultrafilterBasis_is_basis`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_preStoneCechExtend` 📖	mathematical	`Continuous`	`PreStoneCech` `instTopologicalSpacePreStoneCech` `preStoneCechExtend`	—	`continuous_quot_lift` `continuous_ultrafilter_extend`
`continuous_preStoneCechUnit` 📖	mathematical	—	`Continuous` `PreStoneCech` `instTopologicalSpacePreStoneCech` `preStoneCechUnit`	—	`continuous_iff_ultrafilter` `ultrafilter_converges_iff` `Ultrafilter.lawfulMonad` `LE.le.trans` `Filter.map_mono` `Continuous.tendsto` `pure_le_nhds`
`continuous_stoneCechExtend` 📖	mathematical	`Continuous`	`StoneCech` `instTopologicalSpaceStoneCech` `stoneCechExtend`	—	`continuous_coinduced_dom` `continuous_preStoneCechExtend`
`continuous_stoneCechUnit` 📖	mathematical	—	`Continuous` `StoneCech` `instTopologicalSpaceStoneCech` `stoneCechUnit`	—	`Continuous.comp` `continuous_preStoneCechUnit`
`continuous_ultrafilter_extend` 📖	mathematical	—	`Continuous` `Ultrafilter` `Ultrafilter.topologicalSpace` `Ultrafilter.extend`	—	`IsCompact.ultrafilter_le_nhds` `isCompact_univ` `Filter.le_principal_iff` `Filter.univ_mem` `le_trans` `Filter.map_mono` `ultrafilter_comap_pure_nhds` `IsDenseInducing.continuous_extend` `T4Space.t3Space` `instT4SpaceOfT1SpaceOfNormalSpace` `T2Space.t1Space` `NormalSpace.of_regularSpace_lindelofSpace` `instRegularSpaceOfWeaklyLocallyCompactSpaceOfR1Space` `instWeaklyLocallyCompactSpaceOfCompactSpace` `T2Space.r1Space` `instLindelofSpaceOfSigmaCompactSpace` `CompactSpace.sigmaCompact` `isDenseInducing_pure`
`denseRange_preStoneCechUnit` 📖	mathematical	—	`DenseRange` `PreStoneCech` `instTopologicalSpacePreStoneCech` `preStoneCechUnit`	—	`DenseRange.comp` `Function.Surjective.denseRange` `Quot.mk_surjective` `denseRange_pure` `continuous_coinduced_rng`
`denseRange_pure` 📖	mathematical	—	`DenseRange` `Ultrafilter` `Ultrafilter.topologicalSpace` `Ultrafilter.instPure`	—	`mem_closure_iff_ultrafilter` `Filter.range_mem_map` `ultrafilter_converges_iff` `Ultrafilter.lawfulMonad`
`denseRange_stoneCechUnit` 📖	mathematical	—	`DenseRange` `StoneCech` `instTopologicalSpaceStoneCech` `stoneCechUnit`	—	`Quot.mk_surjective` `DenseRange.comp` `Function.Surjective.denseRange` `denseRange_preStoneCechUnit` `continuous_coinduced_rng`
`eq_if_preStoneCechUnit_eq` 📖	—	`Continuous` `preStoneCechUnit`	—	—	`ultrafilter_extend_extends` `preStoneCechCompat` `Quot.eq` `preStoneCechUnit.eq_1`
`eq_if_stoneCechUnit_eq` 📖	—	`Continuous` `stoneCechUnit`	—	—	`stoneCechExtend_extends`
`induced_topology_pure` 📖	mathematical	—	`TopologicalSpace.induced` `Ultrafilter` `Ultrafilter.instPure` `Ultrafilter.topologicalSpace` `Bot.bot` `TopologicalSpace` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`eq_bot_of_singletons_open` `ultrafilter_isOpen_basic`
`instCompactSpacePreStoneCech` 📖	mathematical	—	`CompactSpace` `PreStoneCech` `instTopologicalSpacePreStoneCech`	—	`Quot.compactSpace` `ultrafilter_compact`
`instCompactSpaceStoneCech` 📖	mathematical	—	`CompactSpace` `StoneCech` `instTopologicalSpaceStoneCech`	—	`Quot.compactSpace` `instCompactSpacePreStoneCech`
`instT2SpaceStoneCech` 📖	mathematical	—	`T2Space` `StoneCech` `instTopologicalSpaceStoneCech`	—	`T2Quotient.instT2Space`
`instTotallyDisconnectedSpaceUltrafilter` 📖	mathematical	—	`TotallyDisconnectedSpace` `Ultrafilter` `Ultrafilter.topologicalSpace`	—	`totallyDisconnectedSpace_iff_connectedComponent_singleton` `Ultrafilter.coe_le_coe` `ultrafilter_isClosed_basic` `ultrafilter_isOpen_basic` `Set.mem_iInter` `connectedComponent_eq_iInter_isClopen` `Ultrafilter.t2Space` `ultrafilter_compact`
`isDenseEmbedding_pure` 📖	mathematical	—	`IsDenseEmbedding` `Ultrafilter` `Bot.bot` `TopologicalSpace` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Ultrafilter.topologicalSpace` `Ultrafilter.instPure`	—	`isDenseInducing_pure` `Ultrafilter.pure_injective`
`isDenseInducing_pure` 📖	mathematical	—	`IsDenseInducing` `Ultrafilter` `Bot.bot` `TopologicalSpace` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Ultrafilter.topologicalSpace` `Ultrafilter.instPure`	—	`induced_topology_pure` `denseRange_pure`
`preStoneCechCompat` 📖	mathematical	`Continuous` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Ultrafilter.toFilter` `nhds`	`Ultrafilter.extend`	—	`LE.le.trans` `Filter.map_mono` `Continuous.continuousAt` `ultrafilter_extend_eq_iff` `Ultrafilter.coe_map`
`preStoneCechExtend_extends` 📖	mathematical	`Continuous`	`PreStoneCech` `preStoneCechExtend` `preStoneCechUnit`	—	`ultrafilter_extend_extends`
`preStoneCechExtend_preStoneCechUnit` 📖	mathematical	`Continuous`	`preStoneCechExtend` `preStoneCechUnit`	—	`preStoneCechExtend_extends`
`preStoneCech_hom_ext` 📖	—	`Continuous` `PreStoneCech` `instTopologicalSpacePreStoneCech` `preStoneCechUnit`	—	—	`Continuous.ext_on` `denseRange_preStoneCechUnit`
`stoneCechExtend_extends` 📖	mathematical	`Continuous`	`StoneCech` `stoneCechExtend` `stoneCechUnit`	—	`continuous_preStoneCechExtend` `stoneCechExtend.eq_1` `stoneCechUnit.eq_1` `preStoneCechExtend_extends`
`stoneCechExtend_stoneCechUnit` 📖	mathematical	`Continuous`	`stoneCechExtend` `stoneCechUnit`	—	`stoneCechExtend_extends`
`stoneCech_hom_ext` 📖	—	`Continuous` `StoneCech` `instTopologicalSpaceStoneCech` `stoneCechUnit`	—	—	`Continuous.ext_on` `denseRange_stoneCechUnit`
`ultrafilterBasis_is_basis` 📖	mathematical	—	`TopologicalSpace.IsTopologicalBasis` `Ultrafilter` `Ultrafilter.topologicalSpace` `ultrafilterBasis`	—	`Filter.inter_mem` `Filter.mem_of_superset` `Set.eq_univ_of_univ_subset` `Set.subset_sUnion_of_mem` `Set.eq_univ_of_forall` `Filter.univ_mem`
`ultrafilter_comap_pure_nhds` 📖	mathematical	—	`Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Filter.comap` `Ultrafilter` `Ultrafilter.instPure` `nhds` `Ultrafilter.topologicalSpace` `Ultrafilter.toFilter`	—	`TopologicalSpace.nhds_generateFrom` `Filter.comap_iInf` `iInf_congr_Prop` `Filter.comap_principal` `Filter.le_principal_iff` `iInf_le_of_le` `Filter.principal_mono`
`ultrafilter_compact` 📖	mathematical	—	`CompactSpace` `Ultrafilter` `Ultrafilter.topologicalSpace`	—	`isCompact_iff_ultrafilter_le_nhds` `ultrafilter_converges_iff`
`ultrafilter_converges_iff` 📖	mathematical	—	`Filter` `Ultrafilter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Ultrafilter.toFilter` `nhds` `Ultrafilter.topologicalSpace` `joinM` `Ultrafilter.monad`	—	`Ultrafilter.coe_le_coe` `TopologicalSpace.nhds_generateFrom`
`ultrafilter_extend_eq_iff` 📖	mathematical	—	`Ultrafilter.extend` `Filter` `Preorder.toLE` `PartialOrder.toPreorder` `Filter.instPartialOrder` `Ultrafilter.toFilter` `Ultrafilter.map` `nhds`	—	`ultrafilter_converges_iff` `Ultrafilter.lawfulMonad` `Continuous.tendsto` `continuous_ultrafilter_extend` `le_trans` `ultrafilter_extend_extends` `le_rfl` `Filter.map_mono` `IsDenseInducing.extend_eq_of_tendsto` `isDenseInducing_pure` `ultrafilter_comap_pure_nhds`
`ultrafilter_extend_extends` 📖	mathematical	—	`Ultrafilter` `Ultrafilter.extend` `Ultrafilter.instPure`	—	`IsDenseInducing.extend_eq` `isDenseInducing_pure` `continuous_of_discreteTopology`
`ultrafilter_extend_pure` 📖	mathematical	—	`Ultrafilter.extend` `Ultrafilter` `Ultrafilter.instPure`	—	`ultrafilter_extend_extends`
`ultrafilter_isClosed_basic` 📖	mathematical	—	`IsClosed` `Ultrafilter` `Ultrafilter.topologicalSpace` `setOf` `Set` `Ultrafilter.instMembershipSet`	—	`isOpen_compl_iff` `Set.ext` `Ultrafilter.compl_mem_iff_notMem` `ultrafilter_isOpen_basic`
`ultrafilter_isOpen_basic` 📖	mathematical	—	`IsOpen` `Ultrafilter` `Ultrafilter.topologicalSpace` `setOf` `Set` `Ultrafilter.instMembershipSet`	—	`TopologicalSpace.IsTopologicalBasis.isOpen` `ultrafilterBasis_is_basis`

---

← Back to Index