𝕜 : Type u_2
E : Type u_1
F : Type ?u.18161
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 = ∅
𝕜 : Type u_2
E : Type u_1
F : Type ?u.18161
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
s t : Set E
x y : E
⊢ Set.Nonempty (↑(convexHull 𝕜).toOrderHom s) ↔ Set.Nonempty s
rw [nonempty_iff_ne_empty, nonempty_iff_ne_empty, Ne.def, Ne.def]
no goals
𝕜 : Type u_2
E : Type u_1
F : Type ?u.18161
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 = ∅
exact not_congr convexHull_empty_iff