MetrizableSpace

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

Statistics

Metric	Count
Definitions MetrizableSpace	1
Theorems setOf_continuousAt, MetrizableSpace, instNormalSpaceOfPseudoMetrizableSpace, instPerfectlyNormalSpaceOfPseudoMetrizableSpace, instT4SpaceOfMetrizableSpace, instT6SpaceOfMetrizableSpace	6
Total	7

IsGδ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
setOf_continuousAt 📖	mathematical	—	IsGδ setOf ContinuousAt	—	TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated Filter.HasBasis.exists_antitone_subbasis uniformity_hasBasis_open_symmetric nhds_prod_eq Filter.HasBasis.tendsto_iff Filter.HasBasis.prod_self nhds_basis_opens Filter.HasAntitoneBasis.toHasBasis Set.setOf_forall iInter instCountableNat IsOpen.isGδ isOpen_iff_mem_nhds Filter.mp_mem IsOpen.mem_nhds Filter.univ_mem'

TopologicalSpace

Definitions

Name	Category	Theorems
MetrizableSpace 📖	CompData	16 math math: Topology.IsEmbedding.metrizableSpace, PseudoMetrizableSpace.toMetrizableSpace, Metric.PiNatEmbed.TopologicalSpace.MetrizableSpace.of_countable_separating, IsCompletelyMetrizableSpace.MetrizableSpace, EMetricSpace.metrizableSpace, metrizableSpace_of_t3_secondCountable, ENNReal.instMetrizableSpace, MetrizableSpace.subtype, LightProfinite.instMetrizableSpaceOnePointNat, metrizableSpace_prod, DiscreteTopology.metrizableSpace, Manifold.metrizableSpace, UniformSpace.metrizableSpace, WeakDual.metrizable_of_isCompact, MeasureTheory.instMetrizableSpaceProbabilityMeasure, ContinuousMap.instMetrizableSpace

TopologicalSpace.IsCompletelyMetrizableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
MetrizableSpace 📖	mathematical	—	TopologicalSpace.MetrizableSpace	—	EMetricSpace.metrizableSpace

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instNormalSpaceOfPseudoMetrizableSpace 📖	mathematical	—	NormalSpace	—	CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated
instPerfectlyNormalSpaceOfPseudoMetrizableSpace 📖	mathematical	—	PerfectlyNormalSpace	—	instNormalSpaceOfPseudoMetrizableSpace TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated Filter.HasBasis.exists_antitone_subbasis uniformity_hasBasis_open IsClosed.closure_eq Filter.HasBasis.biInter_biUnion_ball IsGδ.biInter Set.to_countable SetCoe.countable instCountableNat IsOpen.isGδ isOpen_biUnion UniformSpace.isOpen_ball
instT4SpaceOfMetrizableSpace 📖	mathematical	—	T4Space	—	T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace PerfectlyNormalSpace.toNormalSpace instPerfectlyNormalSpaceOfPseudoMetrizableSpace TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace
instT6SpaceOfMetrizableSpace 📖	mathematical	—	T6Space	—	T3Space.toT0Space T4Space.t3Space instT4SpaceOfMetrizableSpace instPerfectlyNormalSpaceOfPseudoMetrizableSpace TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace

---

← Back to Index