case intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.35552
β : Type u_3
ι : Type ?u.35558
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s✝ : Set E
f : E → β
t : Finset ι
w✝ : ι → 𝕜
p : ι → E
s : Finset E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜).toOrderHom ↑s) f
w : E → 𝕜
hw₀ : ∀ (y : E), y ∈ s → 0 ≤ w y
hw₁ : ∑ y in s, w y = 1
hx : centerMass s w _root_.id ∈ ↑(convexHull 𝕜).toOrderHom ↑s
⊢ f (centerMass s w _root_.id) ≤ sup' s (_ : Finset.Nonempty s) f
𝕜 : Type u_2
E : Type u_1
F : Type ?u.35552
β : Type u_3
ι : Type ?u.35558
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s✝ : Set E
f : E → β
t : Finset ι
w : ι → 𝕜
p : ι → E
x : E
s : Finset E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜).toOrderHom ↑s) f
hx : x ∈ ↑(convexHull 𝕜).toOrderHom ↑s
⊢ f x ≤ sup' s (_ : Finset.Nonempty s) f
obtain ⟨w, hw₀, hw₁, rfl⟩ := mem_convexHull.1 hx
no goals
case intro.intro.intro
𝕜 : Type u_2
E : Type u_1
F : Type ?u.35552
β : Type u_3
ι : Type ?u.35558
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s✝ : Set E
f : E → β
t : Finset ι
w✝ : ι → 𝕜
p : ι → E
s : Finset E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜).toOrderHom ↑s) f
w : E → 𝕜
hw₀ : ∀ (y : E), y ∈ s → 0 ≤ w y
hw₁ : ∑ y in s, w y = 1
hx : centerMass s w _root_.id ∈ ↑(convexHull 𝕜).toOrderHom ↑s
⊢ f (centerMass s w _root_.id) ≤ sup' s (_ : Finset.Nonempty s) f
exact (hf.map_centerMass_le hw₀ (by positivity) <| subset_convexHull _ _).trans
  (centerMass_le_sup hw₀ <| by positivity)
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.35552
β : Type u_3
ι : Type ?u.35558
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s✝ : Set E
f : E → β
t : Finset ι
w✝ : ι → 𝕜
p : ι → E
s : Finset E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜).toOrderHom ↑s) f
w : E → 𝕜
hw₀ : ∀ (y : E), y ∈ s → 0 ≤ w y
hw₁ : ∑ y in s, w y = 1
hx : centerMass s w _root_.id ∈ ↑(convexHull 𝕜).toOrderHom ↑s
⊢ 0 < ∑ i in s, w i
positivity
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.35552
β : Type u_3
ι : Type ?u.35558
inst✝⁵ : LinearOrderedField 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : LinearOrderedAddCommGroup β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s✝ : Set E
f : E → β
t : Finset ι
w✝ : ι → 𝕜
p : ι → E
s : Finset E
hf : ConvexOn 𝕜 (↑(convexHull 𝕜).toOrderHom ↑s) f
w : E → 𝕜
hw₀ : ∀ (y : E), y ∈ s → 0 ≤ w y
hw₁ : ∑ y in s, w y = 1
hx : centerMass s w _root_.id ∈ ↑(convexHull 𝕜).toOrderHom ↑s
⊢ 0 < ∑ i in s, w i
positivity