Documentation Verification Report

MetricSpace

📁 Source: Mathlib/Analysis/Convex/MetricSpace.lean

Statistics

Metric	Count
Definitions `ofConvex`, `IsConvexMetricSpace`, `MetricSpace`	3
Theorems `coe_convexCombination`, `dist_convexCombination_map_le'`, `of_convex`, `continuous_convexComboPair`, `continuous_convexComboPair'`, `continuous_convexComboPair_of_isBounded`, `dist_convexCombination_left_le`, `dist_convexCombination_map_le`, `dist_convexCombination_right_le`, `dist_convexComboPair_convexComboPair`, `dist_convexComboPair_convexComboPair_le`, `dist_convexComboPair_left`, `dist_convexComboPair_right`, `dist_left_convexComboPair`, `dist_right_convexComboPair`, `instIsConvexMetricSpace`	16
Total	19

ConvexSpace

Definitions

Name	Category	Theorems
`ofConvex` 📖	CompOp	2 math math: `ofConvex.coe_convexCombination`, `IsConvexMetricSpace.of_convex`

ConvexSpace.ofConvex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_convexCombination` 📖	mathematical	`Convex` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `AddCommGroup.toAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	`Set` `Set.instMembership` `ConvexSpace.convexCombination` `Set.Elem` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `ConvexSpace.ofConvex` `ConvexSpace` `AddTorsor.instConvexSpace` `DivisionRing.toRing` `Field.toDivisionRing` `addGroupIsAddTorsor` `AddCommGroup.toAddGroup` `StdSimplex.map`	—	—

IsConvexMetricSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_convexCombination_map_le'` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `ConvexSpace.convexCombination` `Real.partialOrder` `Real.semiring` `Real.instIsStrictOrderedRing` `StdSimplex.map` `Finsupp.sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Real.instAddCommMonoid` `StdSimplex.weights` `Real.instOne` `Real.instMul`	—	`Real.instIsStrictOrderedRing`
`of_convex` 📖	mathematical	`Convex` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `ESeminormedAddMonoid.toAddMonoid` `ESeminormedAddCommMonoid.toESeminormedAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField`	`IsConvexMetricSpace` `Set.Elem` `ConvexSpace.ofConvex` `Real` `Real.linearOrder` `Real.instField` `Real.instIsStrictOrderedRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `Subtype.metricSpace` `Set` `Set.instMembership` `NormedAddCommGroup.toMetricSpace`	—	`Real.instIsStrictOrderedRing` `LE.le.trans` `StdSimplex.map_map` `instReflLe` `dist_convexCombination_map_le` `instIsConvexMetricSpace`

(root)

Definitions

Name	Category	Theorems
`IsConvexMetricSpace` 📖	CompData	2 math math: `IsConvexMetricSpace.of_convex`, `instIsConvexMetricSpace`
`MetricSpace` 📖	CompData	1 math math: `TopologicalSpace.IsCompletelyMetrizableSpace.complete`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`continuous_convexComboPair` 📖	mathematical	—	`Continuous` `Set.Elem` `Real` `Set.Icc` `Real.instPreorder` `Real.instZero` `Real.instOne` `instTopologicalSpaceProd` `instTopologicalSpaceSubtype` `Set` `Set.instMembership` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `MetricSpace.toPseudoMetricSpace` `convexComboPair` `Real.partialOrder` `Real.semiring` `Real.instIsStrictOrderedRing` `Real.instSub` `Preorder.toLE` `Subtype.prop` `add_sub_cancel` `Real.instAddCommGroup`	—	`Real.instIsStrictOrderedRing` `continuous_prod_of_continuous_lipschitzWith'` `Subtype.prop` `add_sub_cancel` `one_mul` `le_imp_le_of_le_of_le` `dist_convexComboPair_convexComboPair_le` `le_refl` `Prod.dist_eq` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `Real.instIsOrderedRing` `le_max_left` `add_le_add_right` `le_max_right` `add_mul` `Distrib.rightDistribClass` `LipschitzWith.continuous` `mul_comm` `dist_convexComboPair_convexComboPair` `dist_eq_norm` `instReflLe`
`continuous_convexComboPair'` 📖	mathematical	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLE` `Real.instZero` `Real.instOne` `ContinuousOn` `MetricSpace.toPseudoMetricSpace` `Set.preimage` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `convexComboPair` `Real` `Real.partialOrder` `Real.semiring` `Real.instIsStrictOrderedRing` `Real.instSub` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `add_sub_cancel` `Real.instAddCommGroup`	—	`Real.instIsStrictOrderedRing` `continuous_convexComboPair_of_isBounded` `Bornology.IsBounded.all`
`continuous_convexComboPair_of_isBounded` 📖	mathematical	`Continuous` `Real` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `Real.pseudoMetricSpace` `Real.instLE` `Real.instZero` `Real.instOne` `ContinuousOn` `MetricSpace.toPseudoMetricSpace` `Set.preimage` `Compl.compl` `Set` `Set.instCompl` `Set.instSingletonSet` `Bornology.IsBounded` `PseudoMetricSpace.toBornology` `Set.range`	`Continuous` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `MetricSpace.toPseudoMetricSpace` `convexComboPair` `Real` `Real.partialOrder` `Real.semiring` `Real.instIsStrictOrderedRing` `Real.instSub` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `add_sub_cancel` `Real.instAddCommGroup`	—	`Real.instIsStrictOrderedRing` `add_sub_cancel` `Filter.Eventually.exists` `Filter.atTop_neBot` `instIsDirectedOrder` `Real.instIsOrderedRing` `Real.instArchimedean` `Filter.Eventually.and` `Metric.isBounded_iff_eventually` `Bornology.IsBounded.union` `Filter.eventually_gt_atTop` `instNoTopOrderOfNoMaxOrder` `instNoMaxOrderOfNontrivial` `Real.instNontrivial` `Set.mem_range_self` `continuous_iff_continuousAt` `Topology.IsOpenEmbedding.continuousAt_iff` `IsOpen.isOpenEmbedding_subtypeVal` `IsOpen.preimage` `isOpen_Ioo` `OrderTopology.to_orderClosedTopology` `instOrderTopologyReal` `Continuous.continuousAt` `Set.Ioo_subset_Icc_self` `Subtype.prop` `Continuous.comp₃` `continuous_convexComboPair` `Continuous.comp'` `continuous_subtype_val` `ContinuousOn.comp_continuous` `sub_zero` `convexComboPair.congr_simp` `convexComboPair_zero` `Filter.HasBasis.tendsto_right_iff` `Metric.nhds_basis_ball` `Filter.mp_mem` `Nat.instAtLeastTwoHAddOfNat` `Continuous.tendsto'` `Metric.ball_mem_nhds` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `ContinuousOn.continuousAt` `IsOpen.mem_nhds` `Continuous.isOpen_preimage` `IsClosed.isOpen_compl` `isClosed_singleton` `T5Space.toT1Space` `OrderTopology.t5Space` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `Filter.univ_mem'` `lt_imp_lt_of_le_of_le` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `dist_triangle` `le_refl` `add_le_add_left` `dist_convexComboPair_convexComboPair_le` `dist_self` `MulZeroClass.mul_zero` `zero_add` `dist_convexComboPair_right` `mul_le_mul_of_nonneg_right` `IsOrderedRing.toMulPosMono` `sub_le_self` `dist_nonneg` `mul_le_mul_of_nonneg_left` `IsOrderedRing.toPosMulMono` `le_of_lt` `Mathlib.Meta.Positivity.pos_of_isNat` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `add_le_add_right` `LE.le.trans` `le_abs_self` `LT.lt.le` `dist_zero_right` `Mathlib.Tactic.FieldSimp.lt_eq_cancel_lt` `Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul` `Mathlib.Tactic.FieldSimp.subst_add` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval` `Mathlib.Tactic.FieldSimp.NF.one_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval` `Mathlib.Tactic.FieldSimp.NF.atom_eq_eval` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃` `div_one` `one_mul` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval` `Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst` `Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂` `mul_one` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero` `Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero` `ne_of_gt` `Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃` `Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons` `Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div` `Mathlib.Tactic.FieldSimp.NF.eval_cons` `Mathlib.Tactic.FieldSimp.zpow'_one` `Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval_cons_neg` `LT.lt.ne'` `Mathlib.Meta.NormNum.instAtLeastTwo` `Mathlib.Tactic.FieldSimp.NF.cons_pos` `Real.instZeroLEOneClass` `zero_lt_one` `NeZero.one` `GroupWithZero.toNontrivial` `Mathlib.Meta.NormNum.isNat_lt_true` `Mathlib.Meta.NormNum.isNat_add` `sub_self` `convexComboPair_one` `add_zero` `dist_convexComboPair_left` `abs_sub_comm` `div_pos`
`dist_convexCombination_left_le` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `ConvexSpace.convexCombination` `Real.partialOrder` `Real.semiring` `Real.instIsStrictOrderedRing` `Finsupp.sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Real.instAddCommMonoid` `StdSimplex.weights` `Real.instOne` `Real.instMul`	—	`Real.instIsStrictOrderedRing` `StdSimplex.map_id` `StdSimplex.map_const` `ConvexSpace.single` `dist_convexCombination_map_le`
`dist_convexCombination_map_le` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `ConvexSpace.convexCombination` `Real.partialOrder` `Real.semiring` `Real.instIsStrictOrderedRing` `StdSimplex.map` `Finsupp.sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Real.instAddCommMonoid` `StdSimplex.weights` `Real.instOne` `Real.instMul`	—	`Real.instIsStrictOrderedRing` `Function.Injective.extend_apply` `Subtype.val_injective` `StdSimplex.nonempty` `Real.instNontrivial` `Equiv.symm_apply_apply` `StdSimplex.ext` `Finsupp.mapDomain_congr` `Finsupp.sum_mapDomain_index` `MulZeroClass.zero_mul` `add_mul` `Distrib.rightDistribClass` `Finsupp.sum_congr` `IsConvexMetricSpace.dist_convexCombination_map_le'`
`dist_convexCombination_right_le` 📖	mathematical	—	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `ConvexSpace.convexCombination` `Real.partialOrder` `Real.semiring` `Real.instIsStrictOrderedRing` `Finsupp.sum` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `Real.instAddCommMonoid` `StdSimplex.weights` `Real.instOne` `Real.instMul`	—	`Real.instIsStrictOrderedRing` `StdSimplex.map_const` `ConvexSpace.single` `StdSimplex.map_id` `dist_convexCombination_map_le`
`dist_convexComboPair_convexComboPair` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instAdd` `Real.instOne`	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `convexComboPair` `Real` `Real.partialOrder` `Real.semiring` `Real.instIsStrictOrderedRing` `Real.instMul` `abs` `Real.lattice` `Real.instAddGroup` `Real.instSub`	—	`Real.instIsStrictOrderedRing` `Finite.of_fintype` `Fintype.complete` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Finsupp.sum_fintype` `Finset.sum_congr` `Fin.sum_univ_succ` `Matrix.cons_val_succ` `Finset.univ_unique` `Matrix.cons_val_fin_one` `Finset.sum_const` `Finset.card_singleton` `one_smul` `add_sub_cancel` `StdSimplex.ext` `Finsupp.ext` `Finsupp.single_zero` `Finsupp.single_sub` `Finsupp.single_add` `MulZeroClass.zero_mul` `dist_self` `MulZeroClass.mul_zero` `Finset.sum_const_zero` `add_zero` `zero_add` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `Real.instIsDomain` `dist_convexCombination_map_le` `LE.le.antisymm` `le_imp_le_of_le_of_le` `le_refl` `abs_dist_sub_le` `eq_sub_iff_add_eq` `abs_sub_comm` `sub_sub_sub_cancel_left` `dist_convexComboPair_left` `abs_mul` `Real.instIsOrderedRing` `abs_dist` `instReflLe` `dist_comm` `le_of_not_ge`
`dist_convexComboPair_convexComboPair_le` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instAdd` `Real.instOne`	`Real` `Real.instLE` `Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `convexComboPair` `Real.partialOrder` `Real.semiring` `Real.instIsStrictOrderedRing` `Real.instAdd` `Real.instMul`	—	`Real.instIsStrictOrderedRing` `StdSimplex.map_duple` `StdSimplex.duple.congr_simp` `Matrix.cons_val_fin_one` `Finsupp.sum_fintype` `MulZeroClass.zero_mul` `Finset.sum_congr` `Fin.sum_univ_succ` `Finsupp.single_eq_same` `Finsupp.single_eq_of_ne` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `add_zero` `Finset.univ_unique` `zero_add` `Matrix.cons_val_succ` `Finset.sum_singleton` `dist_convexCombination_map_le`
`dist_convexComboPair_left` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instAdd` `Real.instOne`	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `convexComboPair` `Real` `Real.partialOrder` `Real.semiring` `Real.instIsStrictOrderedRing` `Real.instMul`	—	`Real.instIsStrictOrderedRing` `convexComboPair.eq_1` `le_imp_le_of_le_of_le` `dist_convexCombination_left_le` `le_refl` `Finsupp.sum_add_index` `MulZeroClass.zero_mul` `add_mul` `Distrib.rightDistribClass` `Finsupp.sum_single_index` `dist_self` `MulZeroClass.mul_zero` `dist_comm` `zero_add` `instReflLe` `LE.le.antisymm` `eq_sub_iff_add_eq'` `sub_mul` `one_mul` `sub_le_iff_le_add` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `add_comm` `add_le_add_right` `convexComboPair_symm` `dist_triangle_left`
`dist_convexComboPair_right` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instAdd` `Real.instOne`	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `convexComboPair` `Real` `Real.partialOrder` `Real.semiring` `Real.instIsStrictOrderedRing` `Real.instMul`	—	`Real.instIsStrictOrderedRing` `add_comm` `convexComboPair_symm` `dist_convexComboPair_left` `dist_comm`
`dist_left_convexComboPair` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instAdd` `Real.instOne`	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `convexComboPair` `Real` `Real.partialOrder` `Real.semiring` `Real.instIsStrictOrderedRing` `Real.instMul`	—	`Real.instIsStrictOrderedRing` `dist_comm` `dist_convexComboPair_left`
`dist_right_convexComboPair` 📖	mathematical	`Real` `Real.instLE` `Real.instZero` `Real.instAdd` `Real.instOne`	`Dist.dist` `PseudoMetricSpace.toDist` `MetricSpace.toPseudoMetricSpace` `convexComboPair` `Real` `Real.partialOrder` `Real.semiring` `Real.instIsStrictOrderedRing` `Real.instMul`	—	`Real.instIsStrictOrderedRing` `dist_comm` `dist_convexComboPair_right`
`instIsConvexMetricSpace` 📖	mathematical	—	`IsConvexMetricSpace` `AddTorsor.instConvexSpace` `Real` `Real.instRing` `Real.partialOrder` `Real.instIsStrictOrderedRing` `NormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddCommGroup.toSeminormedAddCommGroup` `NormedAddTorsor.toAddTorsor` `MetricSpace.toPseudoMetricSpace`	—	`Real.instIsStrictOrderedRing` `AddTorsor.nonempty` `AddTorsor.convexCombination_eq_affineCombination` `Finset.affineCombination_eq_weightedVSubOfPoint_vadd_of_sum_eq_one` `StdSimplex.total` `Finset.weightedVSubOfPoint_apply` `Finset.sum_congr` `dist_eq_norm_vsub` `vadd_vsub_vadd_cancel_right` `instReflLe` `Finsupp.sum_mapDomain_index` `zero_smul` `add_smul` `vsub_sub_vsub_cancel_right` `Finsupp.sum.eq_1` `le_imp_le_of_le_of_le` `norm_sum_le` `le_refl` `norm_smul` `NormedSpace.toNormSMulClass` `abs_eq_self` `Real.instIsOrderedAddMonoid` `StdSimplex.nonneg`

---

← Back to Index