Convex

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

Statistics

Metric	Count
Definitions	0
Theorems toUniformConvexSpace	1
Total	1

InnerProductSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toUniformConvexSpace 📖	mathematical	—	UniformConvexSpace	—	Nat.instAtLeastTwoHAddOfNat sub_pos_of_lt IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.sqrt_lt' zero_lt_two Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd pow_pos IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing sub_sub_cancel Real.le_sqrt_of_sq_le sq eq_sub_iff_add_eq parallelogram_law_with_norm Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Tactic.Ring.add_congr Nat.cast_one Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add 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 Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pf_left 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.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.nat_rawCast_1 Mathlib.Tactic.RingNF.mul_neg mul_one add_zero Mathlib.Tactic.RingNF.add_neg sub_le_sub_left pow_le_pow_left₀ IsOrderedRing.toPosMulMono Real.instIsOrderedRing IsOrderedRing.toMulPosMono le_of_lt

---

← Back to Index