Documentation Verification Report

Convex

📁 Source: Mathlib/Analysis/Normed/Affine/Convex.lean

Statistics

Metric	Count
Definitions	0
Theorems `exists_subset_interior_convexHull_finset_of_isCompact`, `dist_add_dist`, `dist_add_dist_of_mem_segment`, `exists_mem_interior_convexHull_affineBasis`	4
Total	4

Convex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_subset_interior_convexHull_finset_of_isCompact` 📖	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` `IsCompact` `Set` `Filter` `Filter.instMembership` `nhdsSet`	`Set.instHasSubset` `interior` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `SetLike.coe` `Finset` `Finset.instSetLike`	—	`mem_nhdsSet_iff_exists` `compact_open_separated_add_left` `IsTopologicalAddGroup.toContinuousAdd` `SeminormedAddCommGroup.toIsTopologicalAddGroup` `exists_mem_interior_convexHull_affineBasis` `IsCompact.elim_finite_subcover_image` `IsOpen.add_right` `ContinuousConstVAdd.op` `IsIsometricVAdd.to_continuousConstVAdd` `NormedAddGroup.to_isIsometricVAdd_left` `AddCommSemigroup.isCentralVAdd` `isOpen_interior` `Set.mem_iUnion₂_of_mem` `Set.add_singleton` `Set.image_add_right` `add_neg_cancel` `CanLift.prf` `Set.instCanLiftFinsetCoeFinite` `Finset.coe_add` `Finset.coe_image` `Finset.coe_univ` `Set.image_univ` `convexHull_add` `Real.instIsStrictOrderedRing` `Mathlib.Tactic.GCongr.rel_imp_rel` `Set.instIsTransSubset` `subset_refl` `Set.instReflSubset` `subset_interior_add_left` `Set.iUnion₂_subset_iff` `Mathlib.Tactic.GCongr.imp_right_mono` `Set.add_subset_add` `subset_convexHull` `convexHull_mono` `convexHull_eq`

Wbtw

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_add_dist` 📖	mathematical	`Wbtw` `Real` `Real.instRing` `Real.partialOrder` `SeminormedAddCommGroup.toAddCommGroup` `NormedSpace.toModule` `Real.normedField` `NormedAddTorsor.toAddTorsor`	`Real.instAdd` `Dist.dist` `PseudoMetricSpace.toDist`	—	`dist_left_lineMap` `abs_of_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `dist_lineMap_right` `covariant_swap_add_of_covariant_add` `sub_mul` `one_mul` `add_sub_cancel`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dist_add_dist_of_mem_segment` 📖	mathematical	`Set` `Set.instMembership` `segment` `Real` `Real.semiring` `Real.partialOrder` `AddCommGroup.toAddCommMonoid` `SeminormedAddCommGroup.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SeminormedAddGroup.toAddGroup` `SeminormedAddCommGroup.toSeminormedAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Real.instMonoid` `Module.toDistribMulAction` `NormedSpace.toModule` `Real.normedField`	`Real.instAdd` `Dist.dist` `PseudoMetricSpace.toDist` `SeminormedAddCommGroup.toPseudoMetricSpace`	—	`Wbtw.dist_add_dist` `mem_segment_iff_wbtw` `Real.instIsOrderedRing`
`exists_mem_interior_convexHull_affineBasis` 📖	mathematical	`Set` `Filter` `Filter.instMembership` `nhds` `UniformSpace.toTopologicalSpace` `PseudoMetricSpace.toUniformSpace` `SeminormedAddCommGroup.toPseudoMetricSpace` `NormedAddCommGroup.toSeminormedAddCommGroup`	`Set.instMembership` `interior` `DFunLike.coe` `ClosureOperator` `PartialOrder.toPreorder` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `ClosureOperator.instFunLike` `convexHull` `Real` `Real.semiring` `Real.partialOrder` `ESeminormedAddCommMonoid.toAddCommMonoid` `ENormedAddCommMonoid.toESeminormedAddCommMonoid` `NormedAddCommGroup.toENormedAddCommMonoid` `NormedSpace.toModule` `Real.normedField` `Set.range` `Module.finrank` `AffineBasis` `NormedAddCommGroup.toAddCommGroup` `NormedAddTorsor.toAddTorsor` `SeminormedAddCommGroup.toNormedAddTorsor` `Real.instRing` `AffineBasis.instFunLike` `Set.instHasSubset`	—	`AffineBasis.exists_affineBasis_of_finiteDimensional` `Fintype.card_fin` `Finset.centroid_eq_centerMass` `Real.instIsStrictOrderedRing` `Set.range_add` `convexHull_vadd` `interior_vadd` `IsIsometricVAdd.to_continuousConstVAdd` `NormedAddGroup.to_isIsometricVAdd_left` `neg_neg` `add_zero` `AffineBasis.centroid_mem_interior_convexHull` `Finset.univ_nonempty` `dist_zero_right` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `AddGroup.toOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `Real.instZeroLEOneClass` `Metric.mem_nhds_iff` `Nat.instAtLeastTwoHAddOfNat` `Finset.le_sup'_of_le` `Finset.mem_univ` `norm_nonneg` `Right.add_pos_of_nonneg_of_pos` `Mathlib.Meta.Positivity.pos_of_isNat` `Real.instIsOrderedRing` `Real.instNontrivial` `Mathlib.Meta.NormNum.isNat_ofNat` `Nat.cast_one` `div_pos` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `Mathlib.Meta.NormNum.instAtLeastTwo` `Units.smulCommClass_left` `smulCommClass_self` `LT.lt.ne'` `norm_smul` `NormedSpace.toNormSMulClass` `abs_of_nonneg` `LT.lt.le` `mul_div_right_comm` `div_le_iff₀` `MulPosReflectLE.toMulPosReflectLT` `MulPosStrictMono.toMulPosReflectLE` `IsStrictOrderedRing.toMulPosStrictMono` `IsOrderedRing.toPosMulMono` `Set.range_smul` `convexHull_smul` `interior_smul₀` `UniformContinuousConstSMul.to_continuousConstSMul` `IsBoundedSMul.toUniformContinuousConstSMul` `NormedSpace.toIsBoundedSMul` `Real.instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `convexHull_min` `convex_closedBall` `Metric.closedBall_subset_ball` `lt_of_not_ge` `Mathlib.Tactic.Linarith.lt_irrefl` `Mathlib.Tactic.Ring.of_eq` `Mathlib.Tactic.Ring.add_congr` `Mathlib.Tactic.Ring.sub_congr` `Mathlib.Tactic.Ring.cast_zero` `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` `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.one_mul` `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` `Mathlib.Tactic.Ring.add_pf_add_overlap_zero` `Mathlib.Tactic.Ring.add_overlap_pf_zero` `Mathlib.Tactic.Linarith.add_lt_of_neg_of_le` `Mathlib.Tactic.Linarith.sub_neg_of_lt` `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` `RCLike.charZero_rclike` `Mathlib.Meta.NormNum.isNat_mul` `Mathlib.Tactic.Linarith.mul_nonpos` `Mathlib.Tactic.Linarith.sub_nonpos_of_le` `Mathlib.Meta.NormNum.isNat_lt_true` `neg_add_cancel` `vadd_mem_nhds_vadd`

---

← Back to Index