ExtremallyDisconnected

📁 Source: Mathlib/Topology/ExtremallyDisconnected.lean

Statistics

Metric	Count
Definitions ExtremallyDisconnected, homeoCompactToT2	2
Theorems projective, extremallyDisconnected, projective_iff_extremallyDisconnected, disjoint_closure_of_disjoint_isOpen, open_closure, projective, exists_compact_surjective_zorn_subset, extremallyDisconnected_of_homeo, image_subset_closure_compl_image_compl_of_isOpen, instExtremallyDisconnected, instTotallySeparatedSpaceOfExtremallyDisconnectedOfT2Space	11
Total	13

CompactT2

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
projective_iff_extremallyDisconnected 📖	mathematical	—	Projective ExtremallyDisconnected	—	Projective.extremallyDisconnected ExtremallyDisconnected.projective

CompactT2.ExtremallyDisconnected

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
projective 📖	mathematical	—	CompactT2.Projective	—	isCompact_iff_compactSpace IsClosed.isCompact instCompactSpaceProd isClosed_eq Continuous.comp continuous_fst continuous_snd continuous_subtype_val exists_compact_surjective_zorn_subset T2Space.t1Space ContinuousOn.restrict Continuous.continuousOn Set.mem_univ instT2SpaceSubtype Prod.t2Space Homeomorph.continuous Subtype.mem Function.comp_assoc Homeomorph.self_comp_symm

CompactT2.Projective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extremallyDisconnected 📖	mathematical	CompactT2.Projective	ExtremallyDisconnected	—	Set.disjoint_left IsClosed.prod IsOpen.isClosed_compl T1Space.t1 T2Space.t1Space DiscreteTopology.toT2Space instDiscreteTopologyBool isClosed_closure T4Space.toT1Space instT4SpaceOfT1SpaceOfNormalSpace NormalSpace.of_compactSpace_r1Space Finite.compactSpace Bool.instFinite T2Space.r1Space IsClosed.union Continuous.comp continuous_fst continuous_subtype_val subset_closure Set.mem_singleton isCompact_iff_compactSpace IsClosed.isCompact instCompactSpaceProd instT2SpaceSubtype Prod.t2Space continuous_id HasSubset.Subset.antisymm Set.instAntisymmSubset closure_minimal IsClosed.preimage Set.preimage_comp isClosed_compl_iff Set.preimage_compl Set.preimage_subtype_coe_eq_compl Set.Subset.rfl Disjoint.inter_eq Set.inter_empty

ExtremallyDisconnected

Definitions

Name	Category	Theorems
homeoCompactToT2 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
disjoint_closure_of_disjoint_isOpen 📖	mathematical	Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice IsOpen	Disjoint Set ConditionallyCompletePartialOrderSup.toPartialOrder ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice closure	—	Disjoint.closure_left Disjoint.closure_right open_closure
open_closure 📖	mathematical	IsOpen	IsOpen closure	—	—

StoneCech

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
projective 📖	mathematical	—	CompactT2.Projective StoneCech instTopologicalSpaceStoneCech	—	continuous_of_discreteTopology continuous_stoneCechExtend DenseRange.equalizer denseRange_stoneCechUnit Continuous.comp Function.comp_assoc stoneCechExtend_extends

(root)

Definitions

Name	Category	Theorems
ExtremallyDisconnected 📖	CompData	34 math math: Condensed.instPreservesFiniteProductsOppositeStoneanObjFunctorIsSheafCoherentTopology, Stonean.instExtremallyDisconnectedCarrierToTop, Stonean.instProjective, CompHaus.toStonean_toTop, Stonean.instEffectivelyEnoughCompHausToCompHaus, extremallyDisconnected_of_homeo, Condensed.isSheafStonean, Stonean.instHasExplicitFiniteCoproductsExtremallyDisconnectedCarrier, Stonean.effectiveEpiFamily_tfae, Stonean.epi_iff_surjective, Stonean.instPreregular, Stonean.extremallyDisconnected_pullback, CompactT2.projective_iff_extremallyDisconnected, Stonean.forget.preservesLimits, CompactT2.Projective.extremallyDisconnected, Stonean.instHasPropExtremallyDisconnectedCarrier, Profinite.lift_lifts_assoc, Stonean.instHasExplicitPullbacksOfInclusionsExtremallyDisconnectedCarrier, instExtremallyDisconnected, Profinite.lift_lifts, Condensed.StoneanProfinite.instPreservesEffectiveEpisStoneanProfiniteToProfinite, Condensed.StoneanProfinite.instEffectivelyEnoughStoneanProfiniteToProfinite, CompHaus.presentation.epi_π, Condensed.StoneanProfinite.instReflectsEffectiveEpisStoneanProfiniteToProfinite, Stonean.instReflectsEffectiveEpisCompHausToCompHaus, Stonean.instProjectiveCompHausCompHaus, CompHaus.Gleason, Stonean.instProjectiveProfiniteObjToProfinite, Profinite.presentation.epi_π, Stonean.effectiveEpiFamily_of_jointly_surjective, Stonean.extremallyDisconnected_preimage, CompHaus.instExtremallyDisconnectedCarrierToTopTrueOfProjective, Stonean.instPreservesEffectiveEpisCompHausToCompHaus, Stonean.effectiveEpi_tfae

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_compact_surjective_zorn_subset 📖	mathematical	Continuous	Set CompactSpace Set.Elem instTopologicalSpaceSubtype Set.instMembership Set.image Set.univ	—	isClosed_iInter Set.eq_univ_of_forall Set.inter_nonempty_iff_exists_left IsCompact.nonempty_iInter_of_directed_nonempty_isCompact_isClosed IsChain.symm Set.inter_subset_inter_left Directed.mono_comp directedOn_iff_directed IsChain.directedOn instReflGe Set.image_inter_nonempty_iff Subtype.mem Set.univ_inter Set.singleton_nonempty IsClosed.isCompact IsClosed.inter IsClosed.preimage T1Space.t1 Set.iInter_inter Set.iInter_of_empty not_nonempty_iff Set.image_univ_of_surjective Set.mem_iInter zorn_superset Minimal.prop isCompact_iff_compactSpace Mathlib.Tactic.Contrapose.contrapose₄ Set.eq_univ_of_image_val_eq Minimal.eq_of_subset IsClosed.trans Set.image_image_val_eq_restrict_image Set.image_val_subset
extremallyDisconnected_of_homeo 📖	mathematical	—	ExtremallyDisconnected	—	Topology.IsInducing.closure_eq_preimage_closure_image Homeomorph.isInducing Homeomorph.isOpen_preimage ExtremallyDisconnected.open_closure Homeomorph.isOpen_image
image_subset_closure_compl_image_compl_of_isOpen 📖	mathematical	Continuous IsOpen	Set Set.instHasSubset Set.image closure Compl.compl Set.instCompl	—	Set.image_empty Set.empty_subset mem_closure_iff Set.mem_image Set.mem_inter Set.mem_preimage IsOpen.inter IsOpen.preimage Set.compl_ne_univ IsOpen.isClosed_compl Set.nonempty_compl Set.image_mono Set.mem_image_of_mem Set.mem_compl Set.mem_of_mem_inter_right
instExtremallyDisconnected 📖	mathematical	ExtremallyDisconnected	ExtremallyDisconnected instTopologicalSpaceSigma	—	isOpen_sigma_iff IsOpenMap.preimage_closure_eq_closure_preimage sigma_mk_preimage_image_eq_self sigma_mk_preimage_image' isOpen_empty continuous_sigmaMk
instTotallySeparatedSpaceOfExtremallyDisconnectedOfT2Space 📖	mathematical	—	TotallySeparatedSpace	—	T2Space.t2 ExtremallyDisconnected.open_closure subset_closure Set.mem_compl_iff mem_closure_iff Mathlib.Tactic.Push.not_forall_eq Set.disjoint_iff_inter_eq_empty disjoint_comm Set.union_compl_self disjoint_compl_right

---

← Back to Index