Kuratowski

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

Statistics

Metric	Count
Definitions embeddingOfSubset, kuratowskiEmbedding, kuratowskiEmbedding	3
Theorems embeddingOfSubset_coe, embeddingOfSubset_dist_le, embeddingOfSubset_isometry, exists_isometric_embedding, extend_lp_infty, isometry	6
Total	9

KuratowskiEmbedding

Definitions

Name	Category	Theorems
embeddingOfSubset 📖	CompOp	3 math math: embeddingOfSubset_isometry, embeddingOfSubset_dist_le, embeddingOfSubset_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
embeddingOfSubset_coe 📖	mathematical	—	PreLp Real Real.normedAddCommGroup AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal embeddingOfSubset Real.instSub Dist.dist PseudoMetricSpace.toDist MetricSpace.toPseudoMetricSpace	—	—
embeddingOfSubset_dist_le 📖	mathematical	—	Real Real.instLE Dist.dist PreLp Real.normedAddCommGroup AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal PseudoMetricSpace.toDist SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing lp.inftyNormedCommRing Real.normedCommRing NormedDivisionRing.to_normOneClass NormedField.toNormedDivisionRing Real.normedField embeddingOfSubset MetricSpace.toPseudoMetricSpace	—	lp.norm_le_of_forall_le dist_nonneg Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.sub_congr 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_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add abs_dist_sub_le
embeddingOfSubset_isometry 📖	mathematical	DenseRange UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace	Isometry PreLp Real Real.normedAddCommGroup AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace lp.inftyNormedRing NormedCommRing.toNormedRing Real.normedCommRing NormedDivisionRing.to_normOneClass NormedField.toNormedDivisionRing Real.normedField embeddingOfSubset	—	Isometry.of_dist_eq NormedDivisionRing.to_normOneClass LE.le.antisymm embeddingOfSubset_dist_le le_of_forall_pos_le_add LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing AddGroup.existsAddOfLE contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Nat.instAtLeastTwoHAddOfNat Metric.mem_closure_range_iff half_pos sub_sub_sub_cancel_right dist_triangle dist_comm Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_congr 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_add_gt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add le_imp_le_of_le_of_le le_refl add_le_add_right le_abs_self add_le_add_left covariant_swap_add_of_covariant_add mul_le_mul_of_nonneg_left IsOrderedRing.toPosMulMono Real.instIsOrderedRing le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial dist_eq_norm lp.norm_apply_le_norm ENNReal.top_ne_zero Mathlib.Tactic.Ring.div_congr Mathlib.Tactic.Ring.div_pf Mathlib.Tactic.Ring.inv_single Mathlib.Meta.NormNum.IsNNRat.to_raw_eq Mathlib.Meta.NormNum.isNNRat_inv_pos RCLike.charZero_rclike Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNNRat.of_raw Mathlib.Meta.NormNum.IsNNRat.den_nz
exists_isometric_embedding 📖	mathematical	—	Isometry PreLp Real Real.normedAddCommGroup AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace lp.inftyNormedRing NormedCommRing.toNormedRing Real.normedCommRing NormedDivisionRing.to_normOneClass NormedField.toNormedDivisionRing Real.normedField	—	NormedDivisionRing.to_normOneClass Set.eq_empty_or_nonempty Set.Nonempty.ne_empty Set.mem_univ TopologicalSpace.exists_countable_dense Set.countable_iff_exists_subset_range embeddingOfSubset_isometry Dense.mono

LipschitzOnWith

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extend_lp_infty 📖	mathematical	LipschitzOnWith PreLp Real Real.normedAddCommGroup AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal PseudoMetricSpace.toPseudoEMetricSpace EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace lp.inftyNormedRing NormedCommRing.toNormedRing Real.normedCommRing NormedDivisionRing.to_normOneClass NormedField.toNormedDivisionRing Real.normedField	LipschitzWith Set.EqOn	—	NormedDivisionRing.to_normOneClass extend_real coordinate Set.eq_empty_or_nonempty LipschitzWith.const' LipschitzWith.uniformly_bounded lp.norm_apply_le_norm ENNReal.top_ne_zero LipschitzWith.coordinate lp.ext

NonemptyCompacts

Definitions

Name	Category	Theorems
kuratowskiEmbedding 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
kuratowskiEmbedding 📖	CompOp	1 math math: kuratowskiEmbedding.isometry

kuratowskiEmbedding

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isometry 📖	mathematical	—	Isometry PreLp Real Real.normedAddCommGroup AddSubgroup AddCommGroup.toAddGroup instAddCommGroupPreLp SetLike.instMembership AddSubgroup.instSetLike lp Top.top ENNReal instTopENNReal EMetricSpace.toPseudoEMetricSpace MetricSpace.toEMetricSpace NormedRing.toMetricSpace lp.inftyNormedRing NormedCommRing.toNormedRing Real.normedCommRing NormedDivisionRing.to_normOneClass NormedField.toNormedDivisionRing Real.normedField kuratowskiEmbedding	—	NormedDivisionRing.to_normOneClass KuratowskiEmbedding.exists_isometric_embedding

---

← Back to Index