CantorScheme

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

Statistics

Metric	Count
Definitions Antitone, ClosureAntitone, VanishingDiam, inducedMap	4
Theorems closureAntitone, antitone, map_of_vanishingDiam, map_injective, dist_lt, map_continuous, map_mem	7
Total	11

CantorScheme

Definitions

Name	Category	Theorems
Antitone 📖	MathDef	1 math math: ClosureAntitone.antitone
ClosureAntitone 📖	MathDef	1 math math: Antitone.closureAntitone
VanishingDiam 📖	MathDef	—
inducedMap 📖	CompOp	4 math math: ClosureAntitone.map_of_vanishingDiam, Disjoint.map_injective, map_mem, VanishingDiam.map_continuous

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_mem 📖	mathematical	—	Set Set.instMembership PiNat.res inducedMap	—	Set.Nonempty.some_mem Set.mem_iInter

CantorScheme.Antitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closureAntitone 📖	mathematical	CantorScheme.Antitone IsClosed	CantorScheme.ClosureAntitone	—	HasSubset.Subset.trans Set.instIsTransSubset Eq.subset Set.instReflSubset IsClosed.closure_eq

CantorScheme.ClosureAntitone

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
antitone 📖	mathematical	CantorScheme.ClosureAntitone	CantorScheme.Antitone	—	HasSubset.Subset.trans Set.instIsTransSubset subset_closure
map_of_vanishingDiam 📖	mathematical	CantorScheme.VanishingDiam CantorScheme.ClosureAntitone UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace Set.Nonempty	Set CantorScheme.inducedMap Set.univ	—	Set.eq_univ_iff_forall antitone_nat_of_succ_le antitone Metric.cauchySeq_iff CantorScheme.VanishingDiam.dist_lt cauchySeq_tendsto_of_complete Set.mem_iInter mem_closure_of_tendsto Filter.atTop_neBot instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat Filter.eventually_atTop

CantorScheme.Disjoint

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_injective 📖	mathematical	CantorScheme.Disjoint	Set.Elem Set CantorScheme.inducedMap	—	Subtype.coe_injective PiNat.res_injective Mathlib.Tactic.Contrapose.contrapose₁ Set.not_disjoint_iff PiNat.res_succ CantorScheme.map_mem

CantorScheme.VanishingDiam

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
dist_lt 📖	mathematical	CantorScheme.VanishingDiam Real Real.instLT Real.instZero	Dist.dist PseudoMetricSpace.toDist	—	Nat.instAtLeastTwoHAddOfNat ENNReal.tendsto_atTop_zero lt_of_not_ge Mathlib.Tactic.Linarith.lt_irrefl Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.cast_zero Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Linarith.add_lt_of_neg_of_le Real.instIsStrictOrderedRing Mathlib.Tactic.Linarith.sub_neg_of_lt Real.instIsOrderedRing CancelDenoms.sub_subst CancelDenoms.div_subst Mathlib.Meta.NormNum.isNat_eq_true Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.isNNRat_inv_pos IsStrictOrderedRing.toCharZero Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Linarith.mul_nonpos Mathlib.Tactic.Linarith.sub_nonpos_of_le Mathlib.Meta.NormNum.isNat_lt_true ENNReal.ofReal_lt_ofReal_iff edist_dist lt_of_le_of_lt Metric.edist_le_ediam_of_mem le_refl Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq
map_continuous 📖	mathematical	CantorScheme.VanishingDiam	Continuous Set.Elem Set CantorScheme.inducedMap instTopologicalSpaceSubtype Set.instMembership Pi.topologicalSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace	—	Metric.continuous_iff' dist_lt eventually_nhds_iff Set.mem_setOf PiNat.cylinder_eq_res Set.mem_preimage CantorScheme.map_mem Continuous.isOpen_preimage continuous_subtype_val PiNat.isOpen_cylinder

---

← Back to Index