Lemmas

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

Statistics

Metric	Count
Definitions	0
Theorems instTotallySeparatedSpaceOfCountable, totallySeparatedSpace_of_cardinalMk_lt_continuum, isTotallyDisconnected, totallySeparatedSpace	4
Total	4

CompletelyRegularSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instTotallySeparatedSpaceOfCountable 📖	mathematical	—	TotallySeparatedSpace	—	totallySeparatedSpace_of_cardinalMk_lt_continuum LE.le.trans_lt Cardinal.mk_le_aleph0_iff Cardinal.aleph0_lt_continuum
totallySeparatedSpace_of_cardinalMk_lt_continuum 📖	mathematical	Cardinal Preorder.toLT PartialOrder.toPreorder Cardinal.partialOrder Cardinal.continuum	TotallySeparatedSpace	—	totallySeparatedSpace_of_t0_of_basis_clopen T35Space.toT0Space isTopologicalBasis_clopens_of_cardinalMk_lt_continuum T35Space.toCompletelyRegularSpace

Set.Countable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isTotallyDisconnected 📖	mathematical	—	IsTotallyDisconnected UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace	—	totallyDisconnectedSpace_subtype_iff TotallySeparatedSpace.totallyDisconnectedSpace CompletelyRegularSpace.instTotallySeparatedSpaceOfCountable instT35SpaceSubtype T4Space.instT35Space instT4SpaceOfMetrizableSpace EMetricSpace.metrizableSpace
totallySeparatedSpace 📖	mathematical	—	TotallySeparatedSpace Set.Elem instTopologicalSpaceSubtype Set Set.instMembership	—	CompletelyRegularSpace.instTotallySeparatedSpaceOfCountable instT35SpaceSubtype

---

← Back to Index