Documentation Verification Report

Basic

📁 Source: Mathlib/Topology/Metrizable/Basic.lean

Statistics

Metric	Count
Definitions `PseudoMetrizableSpace`, `pseudoMetrizableSpaceUniformity`	2
Theorems `metrizableSpace`, `exists_countable_dense_subset`, `secondCountableTopology`, `separableSpace`, `subtype`, `toPseudoMetrizableSpace`, `toT0Space`, `exists_countably_generated`, `firstCountableTopology`, `regularSpace`, `subtype`, `toMetrizableSpace`, `instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace`, `metrizableSpace_pi`, `metrizableSpace_prod`, `pseudoMetrizableSpaceUniformity_countably_generated`, `pseudoMetrizableSpace_pi`, `pseudoMetrizableSpace_prod`, `t2Space_of_metrizableSpace`, `metrizableSpace`, `pseudoMetrizableSpace`, `pseudoMetrizableSpace`	22
Total	24

TopologicalSpace

Definitions

Name	Category	Theorems
`PseudoMetrizableSpace` 📖	CompData	10 math math: `MetrizableSpace.toPseudoMetrizableSpace`, `ContinuousMap.instPseudoMetrizableSpace`, `PseudoEMetricSpace.pseudoMetrizableSpace`, `Topology.IsInducing.pseudoMetrizableSpace`, `MeasureTheory.instPseudoMetrizableSpaceProbabilityMeasureOfSeparableSpace`, `UniformSpace.pseudoMetrizableSpace`, `IsCompletelyPseudoMetrizableSpace.PseudoMetrizableSpace`, `pseudoMetrizableSpace_prod`, `PseudoMetrizableSpace.of_regularSpace_secondCountableTopology`, `PseudoMetrizableSpace.subtype`
`pseudoMetrizableSpaceUniformity` 📖	CompOp	1 math math: `pseudoMetrizableSpaceUniformity_countably_generated`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` 📖	mathematical	—	`SecondCountableTopology`	—	`pseudoMetrizableSpaceUniformity_countably_generated` `UniformSpace.has_seq_basis` `Set.countable_iUnion` `instCountableNat` `mem_closure_iff_frequently` `nhds_eq_comap_uniformity` `Filter.frequently_comap` `Filter.HasBasis.frequently_iff` `Filter.HasAntitoneBasis.toHasBasis` `Set.mem_iUnion₂` `Set.eq_univ_iff_forall` `UniformSpace.ball_eq_of_symmetry` `Set.mem_iUnion_of_mem` `LindelofSpace.elim_nhds_subcover` `UniformSpace.ball_mem_nhds` `Filter.HasAntitoneBasis.mem` `UniformSpace.secondCountable_of_separable`
`metrizableSpace_pi` 📖	mathematical	`MetrizableSpace`	`Pi.topologicalSpace`	—	`pseudoMetrizableSpace_pi` `MetrizableSpace.toPseudoMetrizableSpace` `Pi.instT0Space` `MetrizableSpace.toT0Space`
`metrizableSpace_prod` 📖	mathematical	—	`MetrizableSpace` `instTopologicalSpaceProd`	—	`pseudoMetrizableSpace_prod` `MetrizableSpace.toPseudoMetrizableSpace` `Prod.instT0Space` `MetrizableSpace.toT0Space`
`pseudoMetrizableSpaceUniformity_countably_generated` 📖	mathematical	—	`Filter.IsCountablyGenerated` `uniformity` `pseudoMetrizableSpaceUniformity`	—	`PseudoMetrizableSpace.exists_countably_generated`
`pseudoMetrizableSpace_pi` 📖	mathematical	`PseudoMetrizableSpace`	`Pi.topologicalSpace`	—	`pseudoMetrizableSpaceUniformity_countably_generated` `UniformSpace.pseudoMetrizableSpace` `instIsCountablyGeneratedProdForallUniformityOfCountable` `Finite.to_countable`
`pseudoMetrizableSpace_prod` 📖	mathematical	—	`PseudoMetrizableSpace` `instTopologicalSpaceProd`	—	`pseudoMetrizableSpaceUniformity_countably_generated` `UniformSpace.pseudoMetrizableSpace` `instIsCountablyGeneratedProdUniformity`
`t2Space_of_metrizableSpace` 📖	mathematical	—	`T2Space`	—	`T25Space.t2Space` `T3Space.t25Space` `instT3Space` `MetrizableSpace.toT0Space` `PseudoMetrizableSpace.regularSpace` `MetrizableSpace.toPseudoMetrizableSpace`

TopologicalSpace.DiscreteTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`metrizableSpace` 📖	mathematical	—	`TopologicalSpace.MetrizableSpace`	—	`DiscreteTopology.eq_bot` `Filter.isCountablyGenerated_principal` `T1Space.t0Space` `T2Space.t1Space` `DiscreteTopology.toT2Space`

TopologicalSpace.IsSeparable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_countable_dense_subset` 📖	mathematical	`TopologicalSpace.IsSeparable`	`Set` `Set.instHasSubset` `Set.Countable` `closure`	—	`TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated` `UniformSpace.subset_countable_closure_of_almost_dense_set` `UniformSpace.mem_closure_iff_ball` `symmetrize_mem_uniformity` `Set.mem_biUnion` `UniformSpace.ball_mono` `SetRel.symmetrize_subset_inv`
`secondCountableTopology` 📖	mathematical	`TopologicalSpace.IsSeparable`	`SecondCountableTopology` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`Set.Countable.to_subtype` `subset_closure` `Set.countable_range` `Subtype.dense_iff` `Set.range_comp` `Set.val_comp_inclusion` `Subtype.range_coe` `subset_refl` `Set.instReflSubset` `TopologicalSpace.PseudoMetrizableSpace.subtype` `TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated` `UniformSpace.secondCountable_of_separable` `Topology.IsEmbedding.secondCountableTopology` `Topology.IsEmbedding.inclusion`
`separableSpace` 📖	mathematical	`TopologicalSpace.IsSeparable`	`TopologicalSpace.SeparableSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`exists_countable_dense_subset` `CanLift.prf` `Set.canLift` `Subtype.canLift` `Set.countable_of_injective_of_countable_image` `Function.Injective.injOn` `Subtype.coe_injective` `Topology.IsInducing.dense_iff` `Topology.IsInducing.subtypeVal`

TopologicalSpace.MetrizableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`subtype` 📖	mathematical	—	`TopologicalSpace.MetrizableSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`Topology.IsEmbedding.metrizableSpace` `Topology.IsEmbedding.subtypeVal`
`toPseudoMetrizableSpace` 📖	mathematical	—	`TopologicalSpace.PseudoMetrizableSpace`	—	—
`toT0Space` 📖	mathematical	—	`T0Space`	—	—

TopologicalSpace.PseudoMetrizableSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_countably_generated` 📖	mathematical	—	`UniformSpace.toTopologicalSpace` `Filter.IsCountablyGenerated` `uniformity`	—	—
`firstCountableTopology` 📖	mathematical	—	`FirstCountableTopology`	—	`TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated` `UniformSpace.firstCountableTopology`
`regularSpace` 📖	mathematical	—	`RegularSpace`	—	`UniformSpace.to_regularSpace`
`subtype` 📖	mathematical	—	`TopologicalSpace.PseudoMetrizableSpace` `Set.Elem` `instTopologicalSpaceSubtype` `Set` `Set.instMembership`	—	`Topology.IsInducing.pseudoMetrizableSpace` `Topology.IsInducing.subtypeVal`
`toMetrizableSpace` 📖	mathematical	—	`TopologicalSpace.MetrizableSpace`	—	—

Topology.IsEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`metrizableSpace` 📖	mathematical	`Topology.IsEmbedding`	`TopologicalSpace.MetrizableSpace`	—	`Topology.IsInducing.pseudoMetrizableSpace` `TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace` `toIsInducing` `t0Space` `TopologicalSpace.MetrizableSpace.toT0Space`

Topology.IsInducing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pseudoMetrizableSpace` 📖	mathematical	`Topology.IsInducing`	`TopologicalSpace.PseudoMetrizableSpace`	—	`TopologicalSpace.pseudoMetrizableSpaceUniformity_countably_generated` `UniformSpace.toTopologicalSpace_comap` `eq_induced` `Filter.comap.isCountablyGenerated`

UniformSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pseudoMetrizableSpace` 📖	mathematical	—	`TopologicalSpace.PseudoMetrizableSpace` `toTopologicalSpace`	—	—

---

← Back to Index