Loogle!

Result

Found 234 declarations mentioning Convexity.ConvexSpace. Of these, only the first 200 are shown.

• Convexity.ConvexSpace 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  (R : Type u) (M : Type v) [inst₁ : PartialOrder R] [inst₂ : Semiring R] [inst₃ : IsStrictOrderedRing R] : Type (max u v)
• Convexity.IsAffineMap 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  (R : Type u_1) {M : Type u_3} {N : Type u_4} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] [Convexity.ConvexSpace R N] (f : M → N) : Prop
• Convexity.IsAffineMap.id 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] : Convexity.IsAffineMap R id
• Convexity.ConvexSpace.convexCombination_single 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u} {M : Type v} {inst₁ : PartialOrder R} {inst₂ : Semiring R} {inst₃ : IsStrictOrderedRing R} [self : Convexity.ConvexSpace R M] (x : M) : Convexity.sConvexComb (Convexity.StdSimplex.single x) = x
• Convexity.ConvexSpace.sConvexComb_single 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u} {M : Type v} {inst₁ : PartialOrder R} {inst₂ : Semiring R} {inst₃ : IsStrictOrderedRing R} [self : Convexity.ConvexSpace R M] (x : M) : Convexity.sConvexComb (Convexity.StdSimplex.single x) = x
• Convexity.IsAffineMap.const 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {N : Type u_4} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] [Convexity.ConvexSpace R N] (x : N) : Convexity.IsAffineMap R fun x_1 => x
• Convexity.StdSimplex.instConvexSpace 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] : Convexity.ConvexSpace R (Convexity.StdSimplex R I)
• Convexity.ConvexSpace.convexCombination 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u} {M : Type v} [inst₁ : PartialOrder R] [inst₂ : Semiring R] [inst₃ : IsStrictOrderedRing R] [self : Convexity.ConvexSpace R M] (f : Convexity.StdSimplex R M) : M
• Convexity.ConvexSpace.sConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u} {M : Type v} [inst₁ : PartialOrder R] [inst₂ : Semiring R] [inst₃ : IsStrictOrderedRing R] [self : Convexity.ConvexSpace R M] (f : Convexity.StdSimplex R M) : M
• Convexity.iConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (s : Convexity.StdSimplex R I) (f : I → M) : M
• Convexity.iConvexComb_single 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (i : I) (f : I → M) : Convexity.iConvexComb (Convexity.StdSimplex.single i) f = f i
• Convexity.iConvexComb_const 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (s : Convexity.StdSimplex R I) (m : M) : (Convexity.iConvexComb s fun x => m) = m
• Convexity.iConvexComb_id 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (w : Convexity.StdSimplex R M) : Convexity.iConvexComb w id = Convexity.sConvexComb w
• Convexity.iConvexComb_id' 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (w : Convexity.StdSimplex R M) : (Convexity.iConvexComb w fun x => x) = Convexity.sConvexComb w
• Convexity.convexCombPair_one 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {x y : M} : Convexity.convexCombPair 1 0 ⋯ ⋯ ⋯ x y = x
• Convexity.convexCombPair_zero 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {x y : M} : Convexity.convexCombPair 0 1 ⋯ ⋯ ⋯ x y = y
• Convexity.convexComboPair_one 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {x y : M} : Convexity.convexCombPair 1 0 ⋯ ⋯ ⋯ x y = x
• Convexity.convexComboPair_zero 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {x y : M} : Convexity.convexCombPair 0 1 ⋯ ⋯ ⋯ x y = y
• Convexity.sConvexComb_map 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (w : Convexity.StdSimplex R I) (f : I → M) : Convexity.sConvexComb (Convexity.StdSimplex.map f w) = Convexity.iConvexComb w f
• Convexity.IsAffineMap.comp 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] [Convexity.ConvexSpace R N] [Convexity.ConvexSpace R P] {g : N → P} (hg : Convexity.IsAffineMap R g) {f : M → N} (hf : Convexity.IsAffineMap R f) : Convexity.IsAffineMap R (g ∘ f)
• Convexity.iConvexComb_map 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {I : Type u_6} {J : Type u_7} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (s : Convexity.StdSimplex R I) (f : I → J) (g : J → M) : Convexity.iConvexComb (Convexity.StdSimplex.map f s) g = Convexity.iConvexComb s fun i => g (f i)
• Convexity.IsAffineMap.map_sConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {N : Type u_4} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] [Convexity.ConvexSpace R N] {f : M → N} (self : Convexity.IsAffineMap R f) (s : Convexity.StdSimplex R M) : f (Convexity.sConvexComb s) = Convexity.sConvexComb (Convexity.StdSimplex.map f s)
• Convexity.IsAffineMap.mk 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {N : Type u_4} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] [Convexity.ConvexSpace R N] {f : M → N} (map_sConvexComb : ∀ (s : Convexity.StdSimplex R M), f (Convexity.sConvexComb s) = Convexity.sConvexComb (Convexity.StdSimplex.map f s)) : Convexity.IsAffineMap R f
• Convexity.convexCombPair 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t = 1) (x y : M) : M
• Convexity.convexComboPair 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t = 1) (x y : M) : M
• Convexity.IsAffineMap.map_iConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {N : Type u_4} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] [Convexity.ConvexSpace R N] {f : M → N} (hf : Convexity.IsAffineMap R f) (s : Convexity.StdSimplex R I) (g : I → M) : f (Convexity.iConvexComb s g) = Convexity.iConvexComb s (f ∘ g)
• Convexity.convexCombPair_same 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {x : M} : Convexity.convexCombPair s t hs ht h x x = x
• Convexity.convexComboPair_symm 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {x : M} : Convexity.convexCombPair s t hs ht h x x = x
• Convexity.ConvexSpace.assoc 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u} {M : Type v} {inst₁ : PartialOrder R} {inst₂ : Semiring R} {inst₃ : IsStrictOrderedRing R} [self : Convexity.ConvexSpace R M] (f : Convexity.StdSimplex R (Convexity.StdSimplex R M)) : Convexity.sConvexComb (Convexity.StdSimplex.map Convexity.sConvexComb f) = Convexity.sConvexComb f.join
• Convexity.iConvexComb_reindex 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {I : Type u_6} {J : Type u_7} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (s : Convexity.StdSimplex R I) (f : I ≃ J) (g : I → M) : Convexity.iConvexComb s g = Convexity.iConvexComb (Convexity.StdSimplex.map (⇑f) s) (g ∘ ⇑f.symm)
• Convexity.isAffineMap_convexCombPair 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_9} {M : Type u_10} [PartialOrder R] [CommSemiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (m : M) : Convexity.IsAffineMap R (Convexity.convexCombPair s t hs ht h m)
• Convexity.iConvexComb_assoc 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {J : Type u_9} (s : Convexity.StdSimplex R I) (f : I → Convexity.StdSimplex R J) (g : J → M) : (Convexity.iConvexComb s fun i => Convexity.iConvexComb (f i) g) = Convexity.iConvexComb (Convexity.iConvexComb s f) g
• Convexity.iConvexComb_comm 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_9} {M : Type u_10} {I : Type u_11} {J : Type u_12} [PartialOrder R] [CommSemiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (f : Convexity.StdSimplex R I) (g : Convexity.StdSimplex R J) (e : I → J → M) : (Convexity.iConvexComb f fun i => Convexity.iConvexComb g (e i)) = Convexity.iConvexComb g fun j => Convexity.iConvexComb f fun i => e i j
• Convexity.ConvexSpace.mk' 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u} {M : Type v} [inst₁ : PartialOrder R] [inst₂ : Semiring R] [inst₃ : IsStrictOrderedRing R] (sConvexComb : Convexity.StdSimplex R M → M) (sConvexComb_single : ∀ (x : M), sConvexComb (Convexity.StdSimplex.single x) = x) (assoc : ∀ (f : Convexity.StdSimplex R (Convexity.StdSimplex R M)), sConvexComb (Convexity.StdSimplex.map sConvexComb f) = sConvexComb f.join) : Convexity.ConvexSpace R M
• Convexity.iConvexComb_congr 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {w : Convexity.StdSimplex R I} {f g : I → M} (hfg : ∀ (i : I), w.weights i ≠ 0 → f i = g i) : Convexity.iConvexComb w f = Convexity.iConvexComb w g
• Convexity.sConvexComb_sConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (f : Convexity.StdSimplex R (Convexity.StdSimplex R M)) : Convexity.sConvexComb (Convexity.sConvexComb f) = Convexity.sConvexComb (Convexity.StdSimplex.map Convexity.sConvexComb f)
• Convexity.IsAffineMap.map_convexCombPair 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {N : Type u_4} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] [Convexity.ConvexSpace R N] {f : M → N} (hf : Convexity.IsAffineMap R f) {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : M) : f (Convexity.convexCombPair s t hs ht h x y) = Convexity.convexCombPair s t hs ht h (f x) (f y)
• Convexity.ConvexSpace.mk 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_9} (sConvexComb : Convexity.StdSimplex R M → M) (single : ∀ (x : M), sConvexComb (Convexity.StdSimplex.single x) = x) (assoc : ∀ (f : Convexity.StdSimplex R (Convexity.StdSimplex R M)), sConvexComb (Convexity.StdSimplex.map sConvexComb f) = sConvexComb (Convexity.sConvexComb f)) : Convexity.ConvexSpace R M
• Convexity.iConvexComb_assoc' 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {J : Type u_9} (s : Convexity.StdSimplex R I) (f : I → Convexity.StdSimplex R J) (g : I → J → M) : (Convexity.iConvexComb s fun i => Convexity.iConvexComb (f i) (g i)) = Convexity.iConvexComb (Convexity.iConvexComb s fun i => Convexity.StdSimplex.map (fun x => (i, x)) (f i)) (Function.uncurry g)
• Convexity.iConvexComb_assoc'' 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {J : I → Type u_9} (s : Convexity.StdSimplex R I) (f : (i : I) → Convexity.StdSimplex R (J i)) (g : (i : I) → J i → M) : (Convexity.iConvexComb s fun i => Convexity.iConvexComb (f i) (g i)) = Convexity.iConvexComb (Convexity.iConvexComb s fun i => Convexity.StdSimplex.map (fun x => ⟨i, x⟩) (f i)) (Sigma.uncurry g)
• Convexity.sConvexComb_map_iConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (f : I → M) (s : Convexity.StdSimplex R (Convexity.StdSimplex R I)) : Convexity.sConvexComb (Convexity.StdSimplex.map (fun s => Convexity.iConvexComb s f) s) = Convexity.iConvexComb (Convexity.sConvexComb s) f
• Convexity.convexCombPair_symm 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {x y : M} : Convexity.convexCombPair s t hs ht h x y = Convexity.convexCombPair t s ht hs ⋯ y x
• Convexity.iConvexComb_convexCombPair_comm_left 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_9} {M : Type u_10} {I : Type u_11} [PartialOrder R] [CommSemiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (f : Convexity.StdSimplex R I) (m : M) (e : I → M) : (Convexity.iConvexComb f fun x => Convexity.convexCombPair s t hs ht h (e x) m) = Convexity.convexCombPair s t hs ht h (Convexity.iConvexComb f e) m
• Convexity.iConvexComb_convexCombPair_comm_right 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_9} {M : Type u_10} {I : Type u_11} [PartialOrder R] [CommSemiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (f : Convexity.StdSimplex R I) (m : M) (e : I → M) : (Convexity.iConvexComb f fun x => Convexity.convexCombPair s t hs ht h m (e x)) = Convexity.convexCombPair s t hs ht h m (Convexity.iConvexComb f e)
• Convexity.convexCombPair_iConvexComb_left 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {J : Type u_7} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (g : Convexity.StdSimplex R J) (e : J → M) (m : M) : Convexity.convexCombPair s t hs ht h (Convexity.iConvexComb g e) m = Convexity.sConvexComb (Convexity.convexCombPair s t hs ht h (Convexity.StdSimplex.map e g) (Convexity.StdSimplex.single m))
• Convexity.convexCombPair_iConvexComb_right 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {J : Type u_7} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (m : M) (g : Convexity.StdSimplex R J) (e : J → M) : Convexity.convexCombPair s t hs ht h m (Convexity.iConvexComb g e) = Convexity.sConvexComb (Convexity.convexCombPair s t hs ht h (Convexity.StdSimplex.single m) (Convexity.StdSimplex.map e g))
• Convexity.iConvexComb_convexCombPair_comm 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_9} {M : Type u_10} {I : Type u_11} [PartialOrder R] [CommSemiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (f : Convexity.StdSimplex R I) (e₁ e₂ : I → M) : (Convexity.iConvexComb f fun x => Convexity.convexCombPair s t hs ht h (e₁ x) (e₂ x)) = Convexity.convexCombPair s t hs ht h (Convexity.iConvexComb f e₁) (Convexity.iConvexComb f e₂)
• Convexity.sConvexComb_convexCombPair 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) (hst : s + t = 1) (w w' : Convexity.StdSimplex R M) : Convexity.sConvexComb (Convexity.convexCombPair s t hs ht hst w w') = Convexity.convexCombPair s t hs ht hst (Convexity.sConvexComb w) (Convexity.sConvexComb w')
• Convexity.convexCombPair_def 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (p q : M) : Convexity.convexCombPair s t hs ht h p q = Convexity.iConvexComb (Convexity.StdSimplex.duple 0 1 hs ht h) ![p, q]
• Convexity.iConvexComb_convexCombPair 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} {I : Type u_6} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] (s t : I → R) (hs : ∀ (i : I), 0 ≤ s i) (ht : ∀ (i : I), 0 ≤ t i) (h : ∀ (i : I), s i + t i = 1) (f : Convexity.StdSimplex R I) (m₁ m₂ : I → M) : (Convexity.iConvexComb f fun i => Convexity.convexCombPair (s i) (t i) ⋯ ⋯ ⋯ (m₁ i) (m₂ i)) = Convexity.sConvexComb (Convexity.iConvexComb f fun i => Convexity.StdSimplex.duple (m₁ i) (m₂ i) ⋯ ⋯ ⋯)
• Convexity.convexCombPair_iConvexComb_iConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {J₁ : Type u₁} {J₂ : Type u₂} (g₁ : Convexity.StdSimplex R J₁) (g₂ : Convexity.StdSimplex R J₂) (m₁ : J₁ → M) (m₂ : J₂ → M) : Convexity.convexCombPair s t hs ht h (Convexity.iConvexComb g₁ m₁) (Convexity.iConvexComb g₂ m₂) = Convexity.sConvexComb (Convexity.convexCombPair s t hs ht h (Convexity.StdSimplex.map m₁ g₁) (Convexity.StdSimplex.map m₂ g₂))
• Convexity.convexCombPair_convexCombPair_left_eq_sConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {s' t' : R} (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1) (m₁ m₂ m₃ : M) : Convexity.convexCombPair s t hs ht h (Convexity.convexCombPair s' t' hs' ht' h' m₁ m₂) m₃ = Convexity.sConvexComb (Convexity.convexCombPair s t hs ht h (Convexity.StdSimplex.duple m₁ m₂ hs' ht' h') (Convexity.StdSimplex.single m₃))
• Convexity.convexCombPair_convexCombPair_right_eq_sConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {s' t' : R} (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1) (m₁ m₂ m₃ : M) : Convexity.convexCombPair s t hs ht h m₁ (Convexity.convexCombPair s' t' hs' ht' h' m₂ m₃) = Convexity.sConvexComb (Convexity.convexCombPair s t hs ht h (Convexity.StdSimplex.single m₁) (Convexity.StdSimplex.duple m₂ m₃ hs' ht' h'))
• Convexity.convexCombPair_convexCombPair_assoc_left 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {s' t' : R} (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1) {s'' t'' : R} (hs'' : 0 ≤ s'') (ht'' : 0 ≤ t'') (h'' : s'' + t'' = 1) (H : t * s'' = s * t' * t'') (m₁ m₂ m₃ : M) : Convexity.convexCombPair s t hs ht h (Convexity.convexCombPair s' t' hs' ht' h' m₁ m₂) m₃ = Convexity.convexCombPair (s * s') (s * t' + t) ⋯ ⋯ ⋯ m₁ (Convexity.convexCombPair s'' t'' hs'' ht'' h'' m₂ m₃)
• Convexity.convexCombPair_convexCombPair_assoc_right 📋 Mathlib.Geometry.Convex.ConvexSpace.Defs
  {R : Type u_1} {M : Type u_3} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R M] {s t : R} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) {s' t' : R} (hs' : 0 ≤ s') (ht' : 0 ≤ t') (h' : s' + t' = 1) {s'' t'' : R} (hs'' : 0 ≤ s'') (ht'' : 0 ≤ t'') (h'' : s'' + t'' = 1) (H : s * t'' = t * s' * s'') (m₁ m₂ m₃ : M) : Convexity.convexCombPair s t hs ht h m₁ (Convexity.convexCombPair s' t' hs' ht' h' m₂ m₃) = Convexity.convexCombPair (s + t * s') (t * t') ⋯ ⋯ ⋯ (Convexity.convexCombPair s'' t'' hs'' ht'' h'' m₁ m₂) m₃
• Finsupp.instConvexSpace 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
  {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : Type u_4} [Zero X] [Convexity.ConvexSpace R X] : Convexity.ConvexSpace R (ι →₀ X)
• Pi.instConvexSpaceForall 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
  {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → Convexity.ConvexSpace R (X i)] : Convexity.ConvexSpace R ((i : ι) → X i)
• Prod.instConvexSpace 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
  {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] : Convexity.ConvexSpace R (X × Y)
• Prod.isAffineMap_fst 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
  {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] : Convexity.IsAffineMap R Prod.fst
• Prod.isAffineMap_snd 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
  {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] : Convexity.IsAffineMap R Prod.snd
• Pi.isAffineMap_eval 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
  {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → Convexity.ConvexSpace R (X i)] {i : ι} : Convexity.IsAffineMap R fun x => x i
• Finsupp.isAffineMap_eval 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
  {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : Type u_4} [Zero X] [Convexity.ConvexSpace R X] {i : ι} : Convexity.IsAffineMap R fun x => x i
• Pi.sConvexComb_apply 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
  {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → Convexity.ConvexSpace R (X i)] (w : Convexity.StdSimplex R ((i : ι) → X i)) (i : ι) : Convexity.sConvexComb w i = Convexity.iConvexComb w fun x => x i
• Prod.fst_sConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
  {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (w : Convexity.StdSimplex R (X × Y)) : (Convexity.sConvexComb w).1 = Convexity.iConvexComb w Prod.fst
• Prod.snd_sConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
  {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (w : Convexity.StdSimplex R (X × Y)) : (Convexity.sConvexComb w).2 = Convexity.iConvexComb w Prod.snd
• Pi.iConvexComb_apply 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
  {I : Type u_1} {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → Convexity.ConvexSpace R (X i)] (w : Convexity.StdSimplex R I) (f : I → (i : ι) → X i) (i : ι) : Convexity.iConvexComb w f i = Convexity.iConvexComb w fun j => f j i
• Prod.fst_iConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
  {I : Type u_1} {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (w : Convexity.StdSimplex R I) (f : I → X × Y) : (Convexity.iConvexComb w f).1 = Convexity.iConvexComb w fun i => (f i).1
• Prod.snd_iConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
  {I : Type u_1} {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (w : Convexity.StdSimplex R I) (f : I → X × Y) : (Convexity.iConvexComb w f).2 = Convexity.iConvexComb w fun i => (f i).2
• Finsupp.iConvexComb_apply 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
  {I : Type u_1} {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : Type u_4} [Zero X] [Convexity.ConvexSpace R X] (w : Convexity.StdSimplex R I) (f : I → ι →₀ X) (i : ι) : (Convexity.iConvexComb w f) i = Convexity.iConvexComb w fun j => (f j) i
• Finsupp.sConvexComb_apply 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
  {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : Type u_4} [Zero X] [Convexity.ConvexSpace R X] (w : Convexity.StdSimplex R (ι →₀ X)) (i : ι) : (Convexity.sConvexComb w) i = Convexity.iConvexComb w fun x => x i
• Pi.convexCombPair_apply 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
  {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : ι → Type u_4} [(i : ι) → Convexity.ConvexSpace R (X i)] (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (f g : (i : ι) → X i) (i : ι) : Convexity.convexCombPair a b ha hb hab f g i = Convexity.convexCombPair a b ha hb hab (f i) (g i)
• Prod.fst_convexCombPair 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
  {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (x y : X × Y) : (Convexity.convexCombPair a b ha hb hab x y).1 = Convexity.convexCombPair a b ha hb hab x.1 y.1
• Prod.snd_convexCombPair 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
  {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : Type u_3} {Y : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (x y : X × Y) : (Convexity.convexCombPair a b ha hb hab x y).2 = Convexity.convexCombPair a b ha hb hab x.2 y.2
• Finsupp.convexCombPair_apply 📋 Mathlib.Geometry.Convex.ConvexSpace.Prod
  {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_3} {X : Type u_4} [Zero X] [Convexity.ConvexSpace R X] (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (f g : ι →₀ X) (i : ι) : (Convexity.convexCombPair a b ha hb hab f g) i = Convexity.convexCombPair a b ha hb hab (f i) (g i)
• Convexity.IsConvexSet 📋 Mathlib.Geometry.Convex.Set
  (R : Type u_3) {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] (s : Set X) : Prop
• Convexity.IsConvexSet.univ 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] : Convexity.IsConvexSet R Set.univ
• Convexity.IsConvexSet.empty 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] : Convexity.IsConvexSet R ∅
• Convexity.IsConvexSet.of_subsingleton 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {s : Set X} (hs : s.Subsingleton) : Convexity.IsConvexSet R s
• Convexity.IsConvexSet.singleton 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {x : X} : Convexity.IsConvexSet R {x}
• Convexity.ConvexSpace.subtype 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] (s : Set X) (hs : Convexity.IsConvexSet R s) : Convexity.ConvexSpace R ↑s
• Convexity.IsConvexSet.iInter 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {ι : Sort u_7} {s : ι → Set X} (hs : ∀ (i : ι), Convexity.IsConvexSet R (s i)) : Convexity.IsConvexSet R (⋂ i, s i)
• Convexity.IsConvexSet.inter 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {s t : Set X} (hs : Convexity.IsConvexSet R s) (ht : Convexity.IsConvexSet R t) : Convexity.IsConvexSet R (s ∩ t)
• Convexity.IsConvexSet.sInter 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {S : Set (Set X)} (hS : ∀ s ∈ S, Convexity.IsConvexSet R s) : Convexity.IsConvexSet R (⋂₀ S)
• Convexity.IsConvexSet.iInter₂ 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {ι : Sort u_7} {κ : ι → Sort u_8} {s : (i : ι) → κ i → Set X} (h : ∀ (i : ι) (j : κ i), Convexity.IsConvexSet R (s i j)) : Convexity.IsConvexSet R (⋂ i, ⋂ j, s i j)
• Convexity.IsConvexSet.image 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} {Y : Type u_6} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] {f : X → Y} {s : Set X} (hf : Convexity.IsAffineMap R f) (hs : Convexity.IsConvexSet R s) : Convexity.IsConvexSet R (f '' s)
• Convexity.IsConvexSet.preimage 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} {Y : Type u_6} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] {f : X → Y} {s : Set Y} (hf : Convexity.IsAffineMap R f) (hs : Convexity.IsConvexSet R s) : Convexity.IsConvexSet R (f ⁻¹' s)
• Convexity.IsConvexSet.iUnion 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {ι : Sort u_7} {s : ι → Set X} (hs : Directed (fun x1 x2 => x1 ⊆ x2) s) (hs' : ∀ (i : ι), Convexity.IsConvexSet R (s i)) : Convexity.IsConvexSet R (⋃ i, s i)
• Convexity.isAffineMap_subtypeVal 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] (s : Set X) (hs : Convexity.IsConvexSet R s) : Convexity.IsAffineMap R Subtype.val
• Convexity.IsConvexSet.sUnion 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {S : Set (Set X)} (hS : DirectedOn (fun x1 x2 => x1 ⊆ x2) S) (hS' : ∀ s ∈ S, Convexity.IsConvexSet R s) : Convexity.IsConvexSet R (⋃₀ S)
• Convexity.IsConvexSet.pi 📋 Mathlib.Geometry.Convex.Set
  {ι : Type u_1} {R : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {X : ι → Type u_7} [(i : ι) → Convexity.ConvexSpace R (X i)] {s : Set ι} {t : (i : ι) → Set (X i)} (ht : ∀ i ∈ s, Convexity.IsConvexSet R (t i)) : Convexity.IsConvexSet R (s.pi t)
• Convexity.IsConvexSet.prod 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {s : Set X} {Y : Type u_7} [Convexity.ConvexSpace R Y] {t : Set Y} (hs : Convexity.IsConvexSet R s) (ht : Convexity.IsConvexSet R t) : Convexity.IsConvexSet R (s ×ˢ t)
• Convexity.subtypeVal_sConvexComb 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] (s : Set X) (hs : Convexity.IsConvexSet R s) (w : Convexity.StdSimplex R ↑s) : ↑(Convexity.sConvexComb w) = Convexity.iConvexComb w Subtype.val
• Convexity.subtypeVal_iConvexComb 📋 Mathlib.Geometry.Convex.Set
  {I : Type u_2} {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] (s : Set X) (hs : Convexity.IsConvexSet R s) (w : Convexity.StdSimplex R I) (f : I → ↑s) : ↑(Convexity.iConvexComb w f) = Convexity.iConvexComb w fun i => ↑(f i)
• Convexity.IsConvexSet.of_sConvexComb_mem 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {s : Set X} (hs : ∀ (w : Convexity.StdSimplex R X), ↑w.weights.support ⊆ s → Convexity.sConvexComb w ∈ s) : Convexity.IsConvexSet R s
• Convexity.IsConvexSet.sConvexComb_mem 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {w : Convexity.StdSimplex R X} {s : Set X} (hs : Convexity.IsConvexSet R s) (hw : ↑w.weights.support ⊆ s) : Convexity.sConvexComb w ∈ s
• Convexity.IsConvexSet.convexCombPair_mem 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {s : Set X} {x y : X} (hs : Convexity.IsConvexSet R s) (hx : x ∈ s) (hy : y ∈ s) {a b : R} (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : Convexity.convexCombPair a b ha hb hab x y ∈ s
• Convexity.IsConvexSet.iConvexComb_mem 📋 Mathlib.Geometry.Convex.Set
  {ι : Type u_1} {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {s : Set X} (hs : Convexity.IsConvexSet R s) {w : Convexity.StdSimplex R ι} {f : ι → X} (hf : ∀ (i : ι), w.weights i ≠ 0 → f i ∈ s) : Convexity.iConvexComb w f ∈ s
• Convexity.subtypeVal_convexCombPair 📋 Mathlib.Geometry.Convex.Set
  {R : Type u_3} {X : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] (s : Set X) (hs : Convexity.IsConvexSet R s) (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (x y : ↑s) : ↑(Convexity.convexCombPair a b ha hb hab x y) = Convexity.convexCombPair a b ha hb hab ↑x ↑y
• Convexity.IsConvexSet.of_convexCombPair_mem 📋 Mathlib.Geometry.Convex.Set
  {K : Type u_4} {X : Type u_5} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [Convexity.ConvexSpace K X] {s : Set X} (hs : ∀ (a b : K) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), ∀ x ∈ s, ∀ y ∈ s, Convexity.convexCombPair a b ha hb hab x y ∈ s) : Convexity.IsConvexSet K s
• Convexity.IsStarConvexSet 📋 Mathlib.Geometry.Convex.Star
  (R : Type u_1) {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] (x : X) (s : Set X) : Prop
• Convexity.IsStarConvexSet.univ 📋 Mathlib.Geometry.Convex.Star
  {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {x : X} : Convexity.IsStarConvexSet R x Set.univ
• Convexity.IsStarConvexSet.empty 📋 Mathlib.Geometry.Convex.Star
  {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {x : X} : Convexity.IsStarConvexSet R x ∅
• Convexity.IsStarConvexSet.singleton 📋 Mathlib.Geometry.Convex.Star
  {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {x : X} : Convexity.IsStarConvexSet R x {x}
• Convexity.IsStarConvexSet.mem 📋 Mathlib.Geometry.Convex.Star
  {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {x : X} {s : Set X} (hs : Convexity.IsStarConvexSet R x s) (hs₀ : s.Nonempty) : x ∈ s
• Convexity.IsConvexSet.isStarConvexSet 📋 Mathlib.Geometry.Convex.Star
  {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {x : X} {s : Set X} (hs : Convexity.IsConvexSet R s) (hx : x ∈ s) : Convexity.IsStarConvexSet R x s
• Convexity.IsStarConvexSet.iInter 📋 Mathlib.Geometry.Convex.Star
  {R : Type u_1} {X : Type u_2} {ι : Sort u_4} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {x : X} {s : ι → Set X} (hs : ∀ (i : ι), Convexity.IsStarConvexSet R x (s i)) : Convexity.IsStarConvexSet R x (⋂ i, s i)
• Convexity.IsStarConvexSet.iUnion 📋 Mathlib.Geometry.Convex.Star
  {R : Type u_1} {X : Type u_2} {ι : Sort u_4} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {x : X} {s : ι → Set X} (hs : ∀ (i : ι), Convexity.IsStarConvexSet R x (s i)) : Convexity.IsStarConvexSet R x (⋃ i, s i)
• Convexity.IsStarConvexSet.sInter 📋 Mathlib.Geometry.Convex.Star
  {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {x : X} {S : Set (Set X)} (hS : ∀ s ∈ S, Convexity.IsStarConvexSet R x s) : Convexity.IsStarConvexSet R x (⋂₀ S)
• Convexity.IsStarConvexSet.sUnion 📋 Mathlib.Geometry.Convex.Star
  {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {x : X} {S : Set (Set X)} (hS : ∀ s ∈ S, Convexity.IsStarConvexSet R x s) : Convexity.IsStarConvexSet R x (⋃₀ S)
• Convexity.IsStarConvexSet.inter 📋 Mathlib.Geometry.Convex.Star
  {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {x : X} {s t : Set X} (hs : Convexity.IsStarConvexSet R x s) (ht : Convexity.IsStarConvexSet R x t) : Convexity.IsStarConvexSet R x (s ∩ t)
• Convexity.IsStarConvexSet.union 📋 Mathlib.Geometry.Convex.Star
  {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {x : X} {s t : Set X} (hs : Convexity.IsStarConvexSet R x s) (ht : Convexity.IsStarConvexSet R x t) : Convexity.IsStarConvexSet R x (s ∪ t)
• Convexity.IsStarConvexSet.iInter₂ 📋 Mathlib.Geometry.Convex.Star
  {R : Type u_1} {X : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {x : X} {s : (i : ι) → κ i → Set X} (h : ∀ (i : ι) (j : κ i), Convexity.IsStarConvexSet R x (s i j)) : Convexity.IsStarConvexSet R x (⋂ i, ⋂ j, s i j)
• Convexity.IsStarConvexSet.iUnion₂ 📋 Mathlib.Geometry.Convex.Star
  {R : Type u_1} {X : Type u_2} {ι : Sort u_4} {κ : ι → Sort u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] {x : X} {s : (i : ι) → κ i → Set X} (h : ∀ (i : ι) (j : κ i), Convexity.IsStarConvexSet R x (s i j)) : Convexity.IsStarConvexSet R x (⋃ i, ⋃ j, s i j)
• Convexity.IsStarConvexSet.image 📋 Mathlib.Geometry.Convex.Star
  {R : Type u_1} {X : Type u_2} {Y : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] {f : X → Y} {x : X} {s : Set X} (hf : Convexity.IsAffineMap R f) (hs : Convexity.IsStarConvexSet R x s) : Convexity.IsStarConvexSet R (f x) (f '' s)
• Convexity.IsStarConvexSet.preimage 📋 Mathlib.Geometry.Convex.Star
  {R : Type u_1} {X : Type u_2} {Y : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] {f : X → Y} {x : X} {s : Set Y} (hf : Convexity.IsAffineMap R f) (hs : Convexity.IsStarConvexSet R (f x) s) : Convexity.IsStarConvexSet R x (f ⁻¹' s)
• Convexity.IsStarConvexSet.pi 📋 Mathlib.Geometry.Convex.Star
  {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_6} {X : ι → Type u_7} [(i : ι) → Convexity.ConvexSpace R (X i)] {s : Set ι} {x : (i : ι) → X i} {t : (i : ι) → Set (X i)} (ht : ∀ i ∈ s, Convexity.IsStarConvexSet R (x i) (t i)) : Convexity.IsStarConvexSet R x (s.pi t)
• Convexity.IsStarConvexSet.prod 📋 Mathlib.Geometry.Convex.Star
  {R : Type u_1} {X : Type u_2} {Y : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] {x : X} {s : Set X} {t : Set Y} {y : Y} (hs : Convexity.IsStarConvexSet R x s) (ht : Convexity.IsStarConvexSet R y t) : Convexity.IsStarConvexSet R (x, y) (s ×ˢ t)
• Convexity.ConvexSpace.AffineMap 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  (R : Type u_1) [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (X : Type u_2) (Y : Type u_3) [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] : Type (max u_2 u_3)
• Convexity.ConvexSpace.AffineMap.id 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (X : Type u_2) [Convexity.ConvexSpace R X] : Convexity.ConvexSpace.AffineMap R X X
• Convexity.ConvexSpace.AffineMap.const 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (y : Y) : Convexity.ConvexSpace.AffineMap R X Y
• Convexity.ConvexSpace.AffineMap.toFun 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (self : Convexity.ConvexSpace.AffineMap R X Y) : X → Y
• Convexity.ConvexSpace.AffineMap.instFunLike 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] : FunLike (Convexity.ConvexSpace.AffineMap R X Y) X Y
• Convexity.ConvexSpace.AffineMap.mk 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (toFun : X → Y) (isAffineMap_toFun : Convexity.IsAffineMap R toFun := by fun_prop) : Convexity.ConvexSpace.AffineMap R X Y
• Convexity.ConvexSpace.AffineMap.isAffineMap_toFun 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (self : Convexity.ConvexSpace.AffineMap R X Y) : Convexity.IsAffineMap R self.toFun
• Convexity.StdSimplex.affineMapMk 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {X : Type u_3} [Convexity.ConvexSpace R X] (f : M → X) : Convexity.ConvexSpace.AffineMap R (Convexity.StdSimplex R M) X
• Convexity.ConvexSpace.AffineMap.id_apply 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] (X : Type u_2) [Convexity.ConvexSpace R X] (a : X) : (Convexity.ConvexSpace.AffineMap.id X) a = id a
• Convexity.ConvexSpace.AffineMap.comp 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] [Convexity.ConvexSpace R Z] (g : Convexity.ConvexSpace.AffineMap R Y Z) (f : Convexity.ConvexSpace.AffineMap R X Y) : Convexity.ConvexSpace.AffineMap R X Z
• Convexity.ConvexSpace.AffineMap.const_apply 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (y : Y) (x✝ : X) : (Convexity.ConvexSpace.AffineMap.const y) x✝ = y
• Convexity.ConvexSpace.AffineMap.comp_id 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (f : Convexity.ConvexSpace.AffineMap R X Y) : f.comp (Convexity.ConvexSpace.AffineMap.id X) = f
• Convexity.ConvexSpace.AffineMap.id_comp 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (f : Convexity.ConvexSpace.AffineMap R X Y) : (Convexity.ConvexSpace.AffineMap.id Y).comp f = f
• Convexity.ConvexSpace.AffineMap.isAffineMap 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] (f : Convexity.ConvexSpace.AffineMap R X Y) : Convexity.IsAffineMap R ⇑f
• Convexity.StdSimplex.affineMapMk_surjective 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R Y] (s : Convexity.ConvexSpace.AffineMap R (Convexity.StdSimplex R M) Y) : ∃ f, Convexity.StdSimplex.affineMapMk f = s
• Convexity.ConvexSpace.AffineMap.ext 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] {f g : Convexity.ConvexSpace.AffineMap R X Y} (h : ⇑f = ⇑g) : f = g
• Convexity.ConvexSpace.AffineMap.ext_iff 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] {f g : Convexity.ConvexSpace.AffineMap R X Y} : f = g ↔ ⇑f = ⇑g
• Convexity.ConvexSpace.AffineMap.assoc 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} {Z : Type u_4} {T : Type u_5} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] [Convexity.ConvexSpace R Z] [Convexity.ConvexSpace R T] (f₁ : Convexity.ConvexSpace.AffineMap R Z T) (f₂ : Convexity.ConvexSpace.AffineMap R Y Z) (f₃ : Convexity.ConvexSpace.AffineMap R X Y) : (f₁.comp f₂).comp f₃ = f₁.comp (f₂.comp f₃)
• Convexity.ConvexSpace.AffineMap.coe_comp 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] [Convexity.ConvexSpace R Z] (g : Convexity.ConvexSpace.AffineMap R Y Z) (f : Convexity.ConvexSpace.AffineMap R X Y) : ⇑(g.comp f) = ⇑g ∘ ⇑f
• Convexity.ConvexSpace.AffineMap.comp_apply 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [Convexity.ConvexSpace R X] [Convexity.ConvexSpace R Y] [Convexity.ConvexSpace R Z] (g : Convexity.ConvexSpace.AffineMap R Y Z) (f : Convexity.ConvexSpace.AffineMap R X Y) (a✝ : X) : (g.comp f) a✝ = (⇑g ∘ ⇑f) a✝
• Convexity.StdSimplex.affineMapMk_single 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R Y] (f : M → Y) (m : M) : (Convexity.StdSimplex.affineMapMk f) (Convexity.StdSimplex.single m) = f m
• Convexity.StdSimplex.comp_affineMapMk 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {Y : Type u_3} {Z : Type u_4} [Convexity.ConvexSpace R Y] [Convexity.ConvexSpace R Z] (f : Convexity.ConvexSpace.AffineMap R Y Z) (g : M → Y) : f.comp (Convexity.StdSimplex.affineMapMk g) = Convexity.StdSimplex.affineMapMk (⇑f ∘ g)
• Convexity.StdSimplex.affineMapMk_apply 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R Y] (f : M → Y) (s : Convexity.StdSimplex R M) : (Convexity.StdSimplex.affineMapMk f) s = Convexity.iConvexComb s f
• Convexity.StdSimplex.affineMap_ext 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R Y] {f g : Convexity.ConvexSpace.AffineMap R (Convexity.StdSimplex R M) Y} (h : ∀ (i : M), f (Convexity.StdSimplex.single i) = g (Convexity.StdSimplex.single i)) : f = g
• Convexity.StdSimplex.affineMap_ext_iff 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineMap
  {R : Type u_1} [PartialOrder R] [Semiring R] [IsStrictOrderedRing R] {M : Type u_2} {Y : Type u_3} [Convexity.ConvexSpace R Y] {f g : Convexity.ConvexSpace.AffineMap R (Convexity.StdSimplex R M) Y} : f = g ↔ ∀ (i : M), f (Convexity.StdSimplex.single i) = g (Convexity.StdSimplex.single i)
• Convexity.convexSpaceSelf 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] : Convexity.ConvexSpace R R
• Convexity.ConvexSpace.ofModule 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] : Convexity.ConvexSpace R M
• Convexity.IsModuleConvexSpace 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  (R : Type u_2) (M : Type u_3) [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [Convexity.ConvexSpace R M] : Prop
• Convexity.instIsModuleConvexSpaceForall 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] {ι : Type u_6} {M : ι → Type u_7} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [(i : ι) → Convexity.ConvexSpace R (M i)] [∀ (i : ι), Convexity.IsModuleConvexSpace R (M i)] : Convexity.IsModuleConvexSpace R ((i : ι) → M i)
• Convexity.instIsModuleConvexSpaceFinsupp 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] {ι : Type u_6} : Convexity.IsModuleConvexSpace R (ι →₀ M)
• Convexity.instIsModuleConvexSpaceProd 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] [Convexity.ConvexSpace R N] [Convexity.IsModuleConvexSpace R N] : Convexity.IsModuleConvexSpace R (M × N)
• Convexity.IsStarConvexSet.neg 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] {x : M} {s : Set M} (hs : Convexity.IsStarConvexSet R x s) : Convexity.IsStarConvexSet R (-x) (-s)
• Convexity.isConvexSet_coe 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {F : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [SetLike F M] [AddSubmonoidClass F M] [SMulMemClass F R M] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] (S : F) : Convexity.IsConvexSet R ↑S
• Convexity.IsStarConvexSet.add 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] {x y : M} {s t : Set M} (hs : Convexity.IsStarConvexSet R x s) (ht : Convexity.IsStarConvexSet R y t) : Convexity.IsStarConvexSet R (x + y) (s + t)
• Convexity.IsAffineMap.fun_neg 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] [Convexity.ConvexSpace R N] [Convexity.IsModuleConvexSpace R N] {f : M → N} (hf : Convexity.IsAffineMap R f) : Convexity.IsAffineMap R fun i => -f i
• Convexity.instConvexSpaceSubtypeMem 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {F : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [SetLike F M] [AddSubmonoidClass F M] [SMulMemClass F R M] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] (S : F) : Convexity.ConvexSpace R ↥S
• Convexity.IsStarConvexSet.sub 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] {x y : M} {s t : Set M} (hs : Convexity.IsStarConvexSet R x s) (ht : Convexity.IsStarConvexSet R y t) : Convexity.IsStarConvexSet R (x - y) (s - t)
• Convexity.IsAffineMap.neg 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] [Convexity.ConvexSpace R N] [Convexity.IsModuleConvexSpace R N] {f : M → N} (hf : Convexity.IsAffineMap R f) : Convexity.IsAffineMap R (-f)
• Convexity.IsAffineMap.fun_add 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f g : M → N} [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] [Convexity.ConvexSpace R N] [Convexity.IsModuleConvexSpace R N] (hf : Convexity.IsAffineMap R f) (hg : Convexity.IsAffineMap R g) : Convexity.IsAffineMap R fun i => f i + g i
• Convexity.IsAffineMap.add 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f g : M → N} [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] [Convexity.ConvexSpace R N] [Convexity.IsModuleConvexSpace R N] (hf : Convexity.IsAffineMap R f) (hg : Convexity.IsAffineMap R g) : Convexity.IsAffineMap R (f + g)
• Convexity.IsAffineMap.fun_sub 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] [Convexity.ConvexSpace R N] [Convexity.IsModuleConvexSpace R N] {f g : M → N} (hf : Convexity.IsAffineMap R f) (hg : Convexity.IsAffineMap R g) : Convexity.IsAffineMap R fun i => f i - g i
• Convexity.IsAffineMap.sub 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] [Convexity.ConvexSpace R N] [Convexity.IsModuleConvexSpace R N] {f g : M → N} (hf : Convexity.IsAffineMap R f) (hg : Convexity.IsAffineMap R g) : Convexity.IsAffineMap R (f - g)
• Convexity.instIsModuleConvexSpaceSubtypeMem 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {F : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [SetLike F M] [AddSubmonoidClass F M] [SMulMemClass F R M] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] (S : F) : Convexity.IsModuleConvexSpace R ↥S
• convexCombination_eq_sum 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} {inst✝ : Semiring R} {inst✝¹ : PartialOrder R} {inst✝² : IsStrictOrderedRing R} {inst✝³ : AddCommMonoid M} {inst✝⁴ : Module R M} {inst✝⁵ : Convexity.ConvexSpace R M} [self : Convexity.IsModuleConvexSpace R M] (w : Convexity.StdSimplex R M) : Convexity.sConvexComb w = w.weights.sum fun m r => r • m
• Convexity.IsModuleConvexSpace.mk 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [Convexity.ConvexSpace R M] (sConvexComb_eq_sum : ∀ (w : Convexity.StdSimplex R M), Convexity.sConvexComb w = w.weights.sum fun m r => r • m) : Convexity.IsModuleConvexSpace R M
• Convexity.IsModuleConvexSpace.sConvexComb_eq_sum 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} {inst✝ : Semiring R} {inst✝¹ : PartialOrder R} {inst✝² : IsStrictOrderedRing R} {inst✝³ : AddCommMonoid M} {inst✝⁴ : Module R M} {inst✝⁵ : Convexity.ConvexSpace R M} [self : Convexity.IsModuleConvexSpace R M] (w : Convexity.StdSimplex R M) : Convexity.sConvexComb w = w.weights.sum fun m r => r • m
• Convexity.iConvexComb_eq_sum 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} {I : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] (w : Convexity.StdSimplex R I) (f : I → M) : Convexity.iConvexComb w f = w.weights.sum fun i r => r • f i
• Convexity.subtypeVal_submodule_iConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {F : Type u_1} {R : Type u_2} {M : Type u_3} {I : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [SetLike F M] [AddSubmonoidClass F M] [SMulMemClass F R M] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] (S : F) (w : Convexity.StdSimplex R I) (f : I → ↥S) : ↑(Convexity.iConvexComb w f) = Convexity.iConvexComb w fun i => ↑(f i)
• Convexity.subtypeVal_submodule_sConvexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {F : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [SetLike F M] [AddSubmonoidClass F M] [SMulMemClass F R M] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] (S : F) (w : Convexity.StdSimplex R ↥S) : ↑(Convexity.sConvexComb w) = Convexity.iConvexComb w Subtype.val
• Convexity.convexCombPair_eq_sum 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (x y : M) : Convexity.convexCombPair a b ha hb hab x y = a • x + b • y
• Convexity.IsAffineMap.map_sum_weights 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} {N : Type u_4} {I : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M → N} [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] [Convexity.ConvexSpace R N] [Convexity.IsModuleConvexSpace R N] (hf : Convexity.IsAffineMap R f) (w : Convexity.StdSimplex R I) (g : I → M) : f (w.weights.sum fun i r => r • g i) = w.weights.sum fun i r => r • f (g i)
• Convexity.subtypeVal_submodule_convexCombPair 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {F : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [SetLike F M] [AddSubmonoidClass F M] [SMulMemClass F R M] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] (S : F) (a b : R) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (x y : ↥S) : ↑(Convexity.convexCombPair a b ha hb hab x y) = Convexity.convexCombPair a b ha hb hab ↑x ↑y
• Convexity.StdSimplex.affineMapMk_apply_eq_sum_of_fintype 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} {I : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] [Fintype I] (f : I → M) (w : Convexity.StdSimplex R I) : (Convexity.StdSimplex.affineMapMk f) w = ∑ i, w.weights i • f i
• Convexity.StdSimplex.coe_affineMapMk_of_fintype 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} {I : Type u_5} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] [Fintype I] (f : I → M) : ⇑(Convexity.StdSimplex.affineMapMk f) = fun w => ∑ i, w.weights i • f i
• Convexity.IsAffineMap.map_smul_add_smul 📋 Mathlib.Geometry.Convex.ConvexSpace.Module
  {R : Type u_2} {M : Type u_3} {N : Type u_4} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {f : M → N} [Convexity.ConvexSpace R M] [Convexity.IsModuleConvexSpace R M] [Convexity.ConvexSpace R N] [Convexity.IsModuleConvexSpace R N] {a b : R} (hf : Convexity.IsAffineMap R f) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) (x y : M) : f (a • x + b • y) = a • f x + b • f y
• Convexity.ConvexSpace.AffineMap.convex_range 📋 Mathlib.Analysis.Convex.StdSimplex
  {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {X : Type u_3} [Convexity.ConvexSpace R X] {E : Type u_4} [AddCommGroup E] [Module R E] [Convexity.ConvexSpace R E] [Convexity.IsModuleConvexSpace R E] (f : Convexity.ConvexSpace.AffineMap R X E) : Convex R (Set.range ⇑f)
• Set.convexHull_eq_range_iConvexComb 📋 Mathlib.Analysis.Convex.StdSimplex
  {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {E : Type u_3} [AddCommGroup E] [Module R E] [Convexity.ConvexSpace R E] [Convexity.IsModuleConvexSpace R E] (s : Set E) : (convexHull R) s = Set.range ⇑(Convexity.StdSimplex.affineMapMk fun x => ↑x)
• Set.Finite.convexHull_eq_image 📋 Mathlib.Analysis.Convex.StdSimplex
  {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {E : Type u_3} [AddCommGroup E] [Module R E] [Convexity.ConvexSpace R E] [Convexity.IsModuleConvexSpace R E] (s : Set E) : (convexHull R) s = Set.range ⇑(Convexity.StdSimplex.affineMapMk fun x => ↑x)
• Convexity.StdSimplex.continuous_of_isAffineMap 📋 Mathlib.Geometry.Convex.ConvexSpace.ModuleTopology
  {R : Type u_1} {E : Type u_2} {ι : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [Convexity.ConvexSpace R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace R] [IsTopologicalRing R] [ContinuousSMul R E] [Convexity.IsModuleConvexSpace R E] (f : Convexity.StdSimplex R ι → E) (hf : Convexity.IsAffineMap R f) : Continuous f
• Convexity.StdSimplex.continuous_of_affineMap 📋 Mathlib.Geometry.Convex.ConvexSpace.ModuleTopology
  {R : Type u_1} {E : Type u_2} {ι : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup E] [Module R E] [Convexity.ConvexSpace R E] [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace R] [IsTopologicalRing R] [ContinuousSMul R E] [Convexity.IsModuleConvexSpace R E] (f : Convexity.ConvexSpace.AffineMap R (Convexity.StdSimplex R ι) E) : Continuous ⇑f
• AddTorsor.toConvexSpace 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
  {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] : Convexity.ConvexSpace R P
• Convexity.ConvexSpace.ofAddTorsor 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
  {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] : Convexity.ConvexSpace R P
• Convexity.IsAffineConvexSpace 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
  (R : Type u_1) (V : Type u_2) (P : Type u_3) [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [Convexity.ConvexSpace R P] : Prop
• Convexity.IsModuleConvexSpace.isAffineConvexSpace 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
  {R : Type u_1} {V : Type u_2} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [Convexity.ConvexSpace R V] [Convexity.IsModuleConvexSpace R V] : Convexity.IsAffineConvexSpace R V V
• Convexity.IsAffineConvexSpace.mk 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
  {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [Convexity.ConvexSpace R P] (sConvexComb_eq_convexComb : ∀ (w : Convexity.StdSimplex R P), Convexity.sConvexComb w = AddTorsor.convexCombination w) : Convexity.IsAffineConvexSpace R V P
• Convexity.IsAffineConvexSpace.sConvexComb_eq_convexComb 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
  {R : Type u_1} {V : Type u_2} {P : Type u_3} {inst✝ : Ring R} {inst✝¹ : PartialOrder R} {inst✝² : IsStrictOrderedRing R} {inst✝³ : AddCommGroup V} {inst✝⁴ : Module R V} {inst✝⁵ : AddTorsor V P} {inst✝⁶ : Convexity.ConvexSpace R P} [self : Convexity.IsAffineConvexSpace R V P] (w : Convexity.StdSimplex R P) : Convexity.sConvexComb w = AddTorsor.convexCombination w
• AddTorsor.convexCombPair_eq_lineMap 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
  {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [Convexity.ConvexSpace R P] [Convexity.IsAffineConvexSpace R V P] (s t : R) (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : P) : Convexity.convexCombPair s t hs ht h x y = (AffineMap.lineMap y x) s
• AddTorsor.convexCombination_eq_affineCombination 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
  {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [Convexity.ConvexSpace R P] [Convexity.IsAffineConvexSpace R V P] (s : Convexity.StdSimplex R P) : Convexity.sConvexComb s = (Finset.affineCombination R s.weights.support id) ⇑s.weights
• AddTorsor.sConvexComb_eq_affineCombination 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
  {R : Type u_1} {V : Type u_2} {P : Type u_3} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [Convexity.ConvexSpace R P] [Convexity.IsAffineConvexSpace R V P] (s : Convexity.StdSimplex R P) : Convexity.sConvexComb s = (Finset.affineCombination R s.weights.support id) ⇑s.weights
• AddTorsor.iConvexComb_eq_affineCombination 📋 Mathlib.Geometry.Convex.ConvexSpace.AffineSpace
  {R : Type u_1} {V : Type u_2} {P : Type u_3} {I : Type u_4} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [AddCommGroup V] [Module R V] [AddTorsor V P] [Convexity.ConvexSpace R P] [Convexity.IsAffineConvexSpace R V P] (s : Convexity.StdSimplex R I) (f : I → P) : Convexity.iConvexComb s f = (Finset.affineCombination R s.weights.support f) ⇑s.weights
• Convexity.IsConvexDist 📋 Mathlib.Analysis.Convex.MetricSpace
  (X : Type u_2) [inst₁ : Convexity.ConvexSpace ℝ X] [inst₂ : MetricSpace X] : Prop
• Convexity.IsConvexMetricSpace 📋 Mathlib.Analysis.Convex.MetricSpace
  (X : Type u_2) [inst₁ : Convexity.ConvexSpace ℝ X] [inst₂ : MetricSpace X] : Prop
• Convexity.IsConvexDist.subtype 📋 Mathlib.Analysis.Convex.MetricSpace
  {X : Type u_2} [Convexity.ConvexSpace ℝ X] [MetricSpace X] [Convexity.IsConvexDist X] (s : Set X) (hs : Convexity.IsConvexSet ℝ s) : Convexity.IsConvexDist ↑s
• Convexity.dist_sConvexComb_right_le 📋 Mathlib.Analysis.Convex.MetricSpace
  {X : Type u_2} [Convexity.ConvexSpace ℝ X] [MetricSpace X] [Convexity.IsConvexDist X] (x : X) (f : Convexity.StdSimplex ℝ X) : dist x (Convexity.sConvexComb f) ≤ Convexity.iConvexComb f (dist x)
• Convexity.instIsConvexDistOfIsAffineConvexSpaceReal 📋 Mathlib.Analysis.Convex.MetricSpace
  {V : Type u_3} {P : Type u_4} [NormedAddCommGroup V] [NormedSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] [Convexity.ConvexSpace ℝ P] [Convexity.IsAffineConvexSpace ℝ V P] : Convexity.IsConvexDist P
• Convexity.dist_sConvexComb_left_le 📋 Mathlib.Analysis.Convex.MetricSpace
  {X : Type u_2} [Convexity.ConvexSpace ℝ X] [MetricSpace X] [Convexity.IsConvexDist X] (f : Convexity.StdSimplex ℝ X) (x : X) : dist (Convexity.sConvexComb f) x ≤ Convexity.iConvexComb f fun x_1 => dist x_1 x
• Convexity.dist_iConvexComb_left_le 📋 Mathlib.Analysis.Convex.MetricSpace
  {I : Type u_1} {X : Type u_2} [Convexity.ConvexSpace ℝ X] [MetricSpace X] [Convexity.IsConvexDist X] (f : Convexity.StdSimplex ℝ I) (g : I → X) (x : X) : dist (Convexity.iConvexComb f g) x ≤ Convexity.iConvexComb f fun i => dist (g i) x
• Convexity.dist_iConvexComb_right_le 📋 Mathlib.Analysis.Convex.MetricSpace
  {I : Type u_1} {X : Type u_2} [Convexity.ConvexSpace ℝ X] [MetricSpace X] [Convexity.IsConvexDist X] (x : X) (f : Convexity.StdSimplex ℝ I) (g : I → X) : dist x (Convexity.iConvexComb f g) ≤ Convexity.iConvexComb f fun i => dist x (g i)
• Convexity.dist_convexCombination_right_le 📋 Mathlib.Analysis.Convex.MetricSpace
  {X : Type u_2} [Convexity.ConvexSpace ℝ X] [MetricSpace X] [Convexity.IsConvexDist X] {ι : Type u_3} (f : Convexity.StdSimplex ℝ ι) (x y : ι → X) : dist (Convexity.iConvexComb f x) (Convexity.iConvexComb f y) ≤ Convexity.iConvexComb f fun i => dist (x i) (y i)
• Convexity.dist_iConvexComb_le 📋 Mathlib.Analysis.Convex.MetricSpace
  {X : Type u_2} [Convexity.ConvexSpace ℝ X] [MetricSpace X] [Convexity.IsConvexDist X] {ι : Type u_3} (f : Convexity.StdSimplex ℝ ι) (x y : ι → X) : dist (Convexity.iConvexComb f x) (Convexity.iConvexComb f y) ≤ Convexity.iConvexComb f fun i => dist (x i) (y i)
• Convexity.IsConvexDist.dist_iConvexComb_fst_snd_le 📋 Mathlib.Analysis.Convex.MetricSpace
  {X : Type u_2} [inst₁ : Convexity.ConvexSpace ℝ X] [inst₂ : MetricSpace X] [self : Convexity.IsConvexDist X] (f : Convexity.StdSimplex ℝ (X × X)) : dist (Convexity.iConvexComb f Prod.fst) (Convexity.iConvexComb f Prod.snd) ≤ Convexity.iConvexComb f fun x => dist x.1 x.2
• Convexity.IsConvexDist.mk 📋 Mathlib.Analysis.Convex.MetricSpace
  {X : Type u_2} [inst₁ : Convexity.ConvexSpace ℝ X] [inst₂ : MetricSpace X] (dist_iConvexComb_fst_snd_le : ∀ (f : Convexity.StdSimplex ℝ (X × X)), dist (Convexity.iConvexComb f Prod.fst) (Convexity.iConvexComb f Prod.snd) ≤ Convexity.iConvexComb f fun x => dist x.1 x.2) : Convexity.IsConvexDist X
• Convexity.dist_convexCombPair_left 📋 Mathlib.Analysis.Convex.MetricSpace
  {X : Type u_2} [Convexity.ConvexSpace ℝ X] [MetricSpace X] [Convexity.IsConvexDist X] {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) (h : s + t = 1) (x y : X) : dist (Convexity.convexCombPair s t hs ht h x y) x = t * dist x y

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c