Documentation Verification Report

HausdorffAlexandroff

📁 Source: Mathlib/Topology/MetricSpace/HausdorffAlexandroff.lean

Statistics

Metric	Count
Definitions `fromBinary`, `cantorToHilbert`	2
Theorems `fromBinary_continuous`, `fromBinary_surjective`, `cantorToHilbert_continuous`, `cantorToHilbert_surjective`, `exists_nat_bool_continuous_surjective_of_compact`, `exists_retractionCantorSet`	6
Total	8

Real

Definitions

Name	Category	Theorems
`fromBinary` 📖	CompOp	2 math math: `fromBinary_surjective`, `fromBinary_continuous`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`fromBinary_continuous` 📖	mathematical	—	`Continuous` `Set.Elem` `Real` `unitInterval` `Pi.topologicalSpace` `instTopologicalSpaceBool` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `pseudoMetricSpace` `fromBinary`	—	`instDiscreteTopologyBool` `Continuous.comp'` `continuous_ofDigits` `Homeomorph.continuous`
`fromBinary_surjective` 📖	mathematical	—	`Set.Elem` `Real` `unitInterval` `fromBinary`	—	`Subtype.coind_surjective` `instDiscreteTopologyBool` `Set.SurjOn.comp` `ofDigits_SurjOn` `Mathlib.Meta.NormNum.isNat_lt_true` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instCharZero` `Mathlib.Meta.NormNum.isNat_ofNat` `Homeomorph.surjective`

(root)

Definitions

Name	Category	Theorems
`cantorToHilbert` 📖	CompOp	2 math math: `cantorToHilbert_surjective`, `cantorToHilbert_continuous`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cantorToHilbert_continuous` 📖	mathematical	—	`Continuous` `Pi.topologicalSpace` `instTopologicalSpaceBool` `Set.Elem` `Real` `unitInterval` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `cantorToHilbert`	—	`continuous_pi` `Continuous.comp` `Real.fromBinary_continuous` `Continuous.comp'` `continuous_apply` `Homeomorph.continuous`
`cantorToHilbert_surjective` 📖	mathematical	—	`cantorToHilbert`	—	`Function.Surjective.piMap` `Real.fromBinary_surjective` `Homeomorph.surjective`
`exists_nat_bool_continuous_surjective_of_compact` 📖	mathematical	—	`Continuous` `Pi.topologicalSpace` `instTopologicalSpaceBool` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace`	—	`TopologicalSpace.SecondCountableTopology.to_separableSpace` `TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace` `instLindelofSpaceOfSigmaCompactSpace` `CompactSpace.sigmaCompact` `PseudoEMetricSpace.pseudoMetrizableSpace` `Metric.PiNatEmbed.exists_embedding_to_hilbert_cube` `IsClosed.preimage` `cantorToHilbert_continuous` `Topology.IsClosedEmbedding.isClosed_range` `Continuous.isClosedEmbedding` `Pi.t2Space` `instT2SpaceSubtype` `TopologicalSpace.t2Space_of_metrizableSpace` `EMetricSpace.metrizableSpace` `Topology.IsEmbedding.continuous` `Topology.IsEmbedding.injective` `exists_retractionCantorSet` `Set.Nonempty.preimage` `Set.range_nonempty` `cantorToHilbert_surjective` `Subtype.coind_surjective` `Continuous.restrictPreimage` `Set.restrictPreimage_surjective` `Continuous.comp'` `Homeomorph.continuous` `Continuous.subtype_coind` `Homeomorph.surjective`
`exists_retractionCantorSet` 📖	mathematical	`Set.Nonempty`	`Continuous` `Pi.topologicalSpace` `instTopologicalSpaceBool` `Set.range`	—	`instDiscreteTopologyBool` `PiNat.exists_lipschitz_retraction_of_isClosed` `LipschitzWith.continuous`

---

← Back to Index