case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
⊢ ↑f '' ↑(convexHull 𝕜).toOrderHom s ⊆ ↑(convexHull 𝕜).toOrderHom (↑f '' s)

case h₂
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
⊢ ↑(convexHull 𝕜).toOrderHom (↑f '' s) ⊆ ↑f '' ↑(convexHull 𝕜).toOrderHom s
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
⊢ ↑f '' ↑(convexHull 𝕜).toOrderHom s = ↑(convexHull 𝕜).toOrderHom (↑f '' s)
apply Set.Subset.antisymm
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
⊢ ↑(convexHull 𝕜).toOrderHom s ⊆ ↑f ⁻¹' ↑(convexHull 𝕜).toOrderHom (↑f '' s)
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
⊢ ↑f '' ↑(convexHull 𝕜).toOrderHom s ⊆ ↑(convexHull 𝕜).toOrderHom (↑f '' s)
rw [Set.image_subset_iff]
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
⊢ s ⊆ ↑f ⁻¹' ↑(convexHull 𝕜).toOrderHom (↑f '' s)
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
⊢ ↑(convexHull 𝕜).toOrderHom s ⊆ ↑f ⁻¹' ↑(convexHull 𝕜).toOrderHom (↑f '' s)
refine' convexHull_min _ ((convex_convexHull 𝕜 (f '' s)).affine_preimage f)
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
⊢ ↑f '' s ⊆ ↑(convexHull 𝕜).toOrderHom (↑f '' s)
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
⊢ s ⊆ ↑f ⁻¹' ↑(convexHull 𝕜).toOrderHom (↑f '' s)
rw [← Set.image_subset_iff]
no goals
case h₁
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
⊢ ↑f '' s ⊆ ↑(convexHull 𝕜).toOrderHom (↑f '' s)
exact subset_convexHull 𝕜 (f '' s)
no goals
case h₂
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s : Set E
f : E →ᵃ[𝕜] F
⊢ ↑(convexHull 𝕜).toOrderHom (↑f '' s) ⊆ ↑f '' ↑(convexHull 𝕜).toOrderHom s
exact convexHull_min (Set.image_subset _ (subset_convexHull 𝕜 s))
  ((convex_convexHull 𝕜 s).affine_image f)