Perfect

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

Statistics

Metric	Count
Definitions	0
Theorems exists_nat_bool_injection_of_not_countable, exists_nat_bool_injection, small_diam_splitting	3
Total	3

IsClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_nat_bool_injection_of_not_countable 📖	mathematical	Set.Countable	Set Set.instHasSubset Set.range Continuous Pi.topologicalSpace instTopologicalSpaceBool	—	exists_perfect_nonempty_of_isClosed_of_not_countable PolishSpace.toSecondCountableTopology PolishSpace.toIsCompletelyMetrizableSpace Perfect.exists_nat_bool_injection TopologicalSpace.UpgradedIsCompletelyMetrizableSpace.toCompleteSpace HasSubset.Subset.trans Set.instIsTransSubset

Perfect

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_nat_bool_injection 📖	mathematical	Perfect UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.Nonempty	Set Set.instHasSubset Set.range Continuous Pi.topologicalSpace instTopologicalSpaceBool	—	exists_seq_strictAnti_tendsto' ENNReal.instOrderTopology ENNReal.instDenselyOrdered TopologicalSpace.PseudoMetrizableSpace.firstCountableTopology TopologicalSpace.MetrizableSpace.toPseudoMetrizableSpace ENNReal.instMetrizableSpace zero_lt_one' IsOrderedRing.toZeroLEOneClass ENNReal.instIsOrderedRing NeZero.one CantorScheme.Antitone.closureAntitone closed tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds ENNReal.instCanonicallyOrderedAdd instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.eventually_atTop PiNat.res_length Disjoint.symm CantorScheme.ClosureAntitone.map_of_vanishingDiam Set.mem_univ CantorScheme.map_mem Continuous.comp CantorScheme.VanishingDiam.map_continuous instDiscreteTopologyBool continuous_id' CantorScheme.Disjoint.map_injective small_diam_splitting
small_diam_splitting 📖	mathematical	Perfect UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace Set.Nonempty ENNReal Preorder.toLT PartialOrder.toPreorder ENNReal.instPartialOrder instZeroENNReal	Set Set.instHasSubset Preorder.toLE Metric.ediam EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace Disjoint OmegaCompletePartialOrder.toPartialOrder CompleteLattice.instOmegaCompletePartialOrder CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra HeytingAlgebra.toOrderBot Order.Frame.toHeytingAlgebra CompleteDistribLattice.toFrame CompleteBooleanAlgebra.toCompleteDistribLattice	—	splitting T3Space.t25Space T4Space.t3Space instT4SpaceOfT1SpaceOfNormalSpace T2Space.t1Space TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace CompletelyNormalSpace.toNormalSpace UniformSpace.completelyNormalSpace_of_isCountablyGenerated_uniformity EMetric.instIsCountablyGeneratedUniformity Nat.instAtLeastTwoHAddOfNat HasSubset.Subset.trans Set.instIsTransSubset Disjoint.mono

---

← Back to Index