case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.17174
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
⊢ ↑(convexHull 𝕜).toOrderHom s = ∅ → s = ∅

case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.17174
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
⊢ s = ∅ → ↑(convexHull 𝕜).toOrderHom s = ∅
𝕜 : Type u_2
E : Type u_1
F : Type ?u.17174
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
⊢ ↑(convexHull 𝕜).toOrderHom s = ∅ ↔ s = ∅
constructor
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.17174
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
h : ↑(convexHull 𝕜).toOrderHom s = ∅
⊢ s = ∅
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.17174
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
⊢ ↑(convexHull 𝕜).toOrderHom s = ∅ → s = ∅
intro h
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.17174
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
h : ↑(convexHull 𝕜).toOrderHom s = ∅
⊢ s ⊆ ↑(convexHull 𝕜).toOrderHom s
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.17174
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
h : ↑(convexHull 𝕜).toOrderHom s = ∅
⊢ s = ∅
rw [← Set.subset_empty_iff, ← h]
no goals
case mp
𝕜 : Type u_2
E : Type u_1
F : Type ?u.17174
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
h : ↑(convexHull 𝕜).toOrderHom s = ∅
⊢ s ⊆ ↑(convexHull 𝕜).toOrderHom s
exact subset_convexHull 𝕜 _
case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.17174
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
t : Set E
x y : E
⊢ ↑(convexHull 𝕜).toOrderHom ∅ = ∅
case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.17174
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
⊢ s = ∅ → ↑(convexHull 𝕜).toOrderHom s = ∅
rintro rfl
no goals
case mpr
𝕜 : Type u_2
E : Type u_1
F : Type ?u.17174
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
t : Set E
x y : E
⊢ ↑(convexHull 𝕜).toOrderHom ∅ = ∅
exact convexHull_empty