GDelta

📁 Source: Mathlib/Topology/Separation/GDelta.lean

Statistics

Metric	Count
Definitions PerfectlyNormalSpace, T6Space	2
Theorems hasSeparatingCover_closed_gdelta_right, isGδ_compl, isGδ, compl_singleton, singleton, closed_gdelta, toCompletelyNormalSpace, toNormalSpace, isGδ_compl, isGδ, isGδ_compl, isGδ_compl, toPerfectlyNormalSpace, toT0Space, toT5Space, instR0SpaceOfPerfectlyNormalSpace	16
Total	18

Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasSeparatingCover_closed_gdelta_right 📖	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 IsGδ	HasSeparatingCover	—	Set.eq_empty_or_nonempty Set.disjoint_univ Set.sInter_empty Set.hasSeparatingCover_empty_left Set.Countable.exists_surjective HasSubset.Subset.antisymm Set.instAntisymmSubset Set.subset_iInter HasSubset.Subset.trans Set.instIsTransSubset subset_closure Set.subset_sInter Set.iInter_subset_of_subset subset_refl Set.instReflSubset Set.compl_iInter Set.subset_compl_comm subset_compl_left isOpen_compl_iff isClosed_closure closure_compl closure_eq_iff_isClosed IsOpen.subset_interior_closure normal_exists_closure_subset Set.sInter_subset_of_mem

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGδ_compl 📖	mathematical	—	IsGδ Compl.compl Set Set.instCompl SetLike.coe Finset instSetLike	—	Set.Finite.isGδ_compl finite_toSet

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGδ 📖	mathematical	—	IsGδ	—	PerfectlyNormalSpace.closed_gdelta

IsGδ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
compl_singleton 📖	mathematical	—	IsGδ Compl.compl Set Set.instCompl Set.instSingletonSet	—	IsOpen.isGδ isOpen_compl_singleton
singleton 📖	mathematical	—	IsGδ Set Set.instSingletonSet	—	Filter.HasBasis.exists_antitone_subbasis FirstCountableTopology.nhds_generated_countable nhds_basis_opens biInter_basis_nhds Filter.HasAntitoneBasis.toHasBasis biInter Set.to_countable SetCoe.countable instCountableNat IsOpen.isGδ

PerfectlyNormalSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closed_gdelta 📖	mathematical	—	IsGδ	—	—
toCompletelyNormalSpace 📖	mathematical	—	CompletelyNormalSpace	—	separatedNhds_iff_disjoint hasSeparatingCovers_iff_separatedNhds HasSeparatingCover.mono Disjoint.hasSeparatingCover_closed_gdelta_right toNormalSpace isClosed_closure closed_gdelta subset_closure Disjoint.symm
toNormalSpace 📖	mathematical	—	NormalSpace	—	—

Set.Countable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGδ_compl 📖	mathematical	—	IsGδ Compl.compl Set Set.instCompl	—	Set.biUnion_of_singleton Set.compl_iUnion₂ IsGδ.biInter IsGδ.compl_singleton

Set.Finite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGδ 📖	mathematical	—	IsGδ	—	induction_on IsGδ.empty IsGδ.union IsGδ.singleton
isGδ_compl 📖	mathematical	—	IsGδ Compl.compl Set Set.instCompl	—	Set.Countable.isGδ_compl countable

Set.Subsingleton

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isGδ_compl 📖	mathematical	Set.Subsingleton	IsGδ Compl.compl Set Set.instCompl	—	Set.Finite.isGδ_compl finite

T6Space

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toPerfectlyNormalSpace 📖	mathematical	—	PerfectlyNormalSpace	—	—
toT0Space 📖	mathematical	—	T0Space	—	—
toT5Space 📖	mathematical	—	T5Space	—	instT1SpaceOfT0SpaceOfR0Space toT0Space instR0SpaceOfPerfectlyNormalSpace toPerfectlyNormalSpace PerfectlyNormalSpace.toCompletelyNormalSpace

(root)

Definitions

Name	Category	Theorems
PerfectlyNormalSpace 📖	CompData	2 math math: instPerfectlyNormalSpaceOfPseudoMetrizableSpace, T6Space.toPerfectlyNormalSpace
T6Space 📖	CompData	1 math math: instT6SpaceOfMetrizableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instR0SpaceOfPerfectlyNormalSpace 📖	mathematical	—	R0Space	—	specializes_iff_forall_closed IsClosed.isGδ Set.mem_sInter Specializes.mem_open

---

← Back to Index