𝕜 : Type u_2
E : Type u_1
ι : Type ?u.41306
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
⊢ (∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜).toOrderHom t ⊆ t) ↔
    ∀ (x : E), x ∈ s → ¬x ∈ ↑(convexHull 𝕜).toOrderHom (s \ {x})
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.41306
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
⊢ ConvexIndependent 𝕜 Subtype.val ↔ ∀ (x : E), x ∈ s → ¬x ∈ ↑(convexHull 𝕜).toOrderHom (s \ {x})
rw [convexIndependent_set_iff_inter_convexHull_subset]
case mp
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.41306
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
⊢ (∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜).toOrderHom t ⊆ t) →
    ∀ (x : E), x ∈ s → ¬x ∈ ↑(convexHull 𝕜).toOrderHom (s \ {x})

case mpr
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.41306
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
⊢ (∀ (x : E), x ∈ s → ¬x ∈ ↑(convexHull 𝕜).toOrderHom (s \ {x})) →
    ∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜).toOrderHom t ⊆ t
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.41306
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
⊢ (∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜).toOrderHom t ⊆ t) ↔
    ∀ (x : E), x ∈ s → ¬x ∈ ↑(convexHull 𝕜).toOrderHom (s \ {x})
constructor
case mp
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.41306
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
hs : ∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜).toOrderHom t ⊆ t
x : E
hxs : x ∈ s
hx : x ∈ ↑(convexHull 𝕜).toOrderHom (s \ {x})
⊢ False
case mp
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.41306
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
⊢ (∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜).toOrderHom t ⊆ t) →
    ∀ (x : E), x ∈ s → ¬x ∈ ↑(convexHull 𝕜).toOrderHom (s \ {x})
rintro hs x hxs hx
no goals
case mp
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.41306
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
hs : ∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜).toOrderHom t ⊆ t
x : E
hxs : x ∈ s
hx : x ∈ ↑(convexHull 𝕜).toOrderHom (s \ {x})
⊢ False
exact (hs _ (Set.diff_subset _ _) ⟨hxs, hx⟩).2 (Set.mem_singleton _)
case mpr.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.41306
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hs : ∀ (x : E), x ∈ s → ¬x ∈ ↑(convexHull 𝕜).toOrderHom (s \ {x})
t : Set E
ht : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ ↑(convexHull 𝕜).toOrderHom t
⊢ x ∈ t
case mpr
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.41306
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
⊢ (∀ (x : E), x ∈ s → ¬x ∈ ↑(convexHull 𝕜).toOrderHom (s \ {x})) →
    ∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜).toOrderHom t ⊆ t
rintro hs t ht x ⟨hxs, hxt⟩
case mpr.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.41306
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hs : ∀ (x : E), x ∈ s → ¬x ∈ ↑(convexHull 𝕜).toOrderHom (s \ {x})
t : Set E
ht : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ ↑(convexHull 𝕜).toOrderHom t
h : ¬x ∈ t
⊢ False
case mpr.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.41306
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hs : ∀ (x : E), x ∈ s → ¬x ∈ ↑(convexHull 𝕜).toOrderHom (s \ {x})
t : Set E
ht : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ ↑(convexHull 𝕜).toOrderHom t
⊢ x ∈ t
by_contra h
no goals
case mpr.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.41306
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hs : ∀ (x : E), x ∈ s → ¬x ∈ ↑(convexHull 𝕜).toOrderHom (s \ {x})
t : Set E
ht : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ ↑(convexHull 𝕜).toOrderHom t
h : ¬x ∈ t
⊢ False
exact hs _ hxs (convexHull_mono (Set.subset_diff_singleton ht h) hxt)