𝕜 : Type u_2
E : Type u_1
F : Type ?u.45458
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
⊢ affineSpan 𝕜 (↑(convexHull 𝕜).toOrderHom s) ≤ affineSpan 𝕜 s
𝕜 : Type u_2
E : Type u_1
F : Type ?u.45458
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
⊢ affineSpan 𝕜 (↑(convexHull 𝕜).toOrderHom s) = affineSpan 𝕜 s
refine' le_antisymm _ (affineSpan_mono 𝕜 (subset_convexHull 𝕜 s))
𝕜 : Type u_2
E : Type u_1
F : Type ?u.45458
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
⊢ ↑(convexHull 𝕜).toOrderHom s ⊆ ↑(affineSpan 𝕜 s)
𝕜 : Type u_2
E : Type u_1
F : Type ?u.45458
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
⊢ affineSpan 𝕜 (↑(convexHull 𝕜).toOrderHom s) ≤ affineSpan 𝕜 s
rw [affineSpan_le]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.45458
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
⊢ ↑(convexHull 𝕜).toOrderHom s ⊆ ↑(affineSpan 𝕜 s)
exact convexHull_subset_affineSpan s