case mp
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39598
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
⊢ ConvexIndependent 𝕜 Subtype.val → ∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜).toOrderHom t ⊆ t

case mpr
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39598
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
⊢ (∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜).toOrderHom t ⊆ t) → ConvexIndependent 𝕜 Subtype.val
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39598
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
⊢ ConvexIndependent 𝕜 Subtype.val ↔ ∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜).toOrderHom t ⊆ t
constructor
case mp.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39598
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hc : ConvexIndependent 𝕜 Subtype.val
t : Set E
h : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ ↑(convexHull 𝕜).toOrderHom t
⊢ x ∈ t
case mp
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39598
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
⊢ ConvexIndependent 𝕜 Subtype.val → ∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜).toOrderHom t ⊆ t
rintro hc t h x ⟨hxs, hxt⟩
case mp.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39598
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hc : ConvexIndependent 𝕜 Subtype.val
t : Set E
h : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ ↑(convexHull 𝕜).toOrderHom t
⊢ ↑{ val := x, property := hxs } ∈ ↑(convexHull 𝕜).toOrderHom (Subtype.val '' {x | ↑x ∈ t})
case mp.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39598
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hc : ConvexIndependent 𝕜 Subtype.val
t : Set E
h : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ ↑(convexHull 𝕜).toOrderHom t
⊢ x ∈ t
refine' hc { x | ↑x ∈ t } ⟨x, hxs⟩ _
case mp.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39598
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hc : ConvexIndependent 𝕜 Subtype.val
t : Set E
h : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ ↑(convexHull 𝕜).toOrderHom t
⊢ ↑{ val := x, property := hxs } ∈ ↑(convexHull 𝕜).toOrderHom t
case mp.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39598
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hc : ConvexIndependent 𝕜 Subtype.val
t : Set E
h : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ ↑(convexHull 𝕜).toOrderHom t
⊢ ↑{ val := x, property := hxs } ∈ ↑(convexHull 𝕜).toOrderHom (Subtype.val '' {x | ↑x ∈ t})
rw [Subtype.coe_image_of_subset h]
no goals
case mp.intro
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39598
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hc : ConvexIndependent 𝕜 Subtype.val
t : Set E
h : t ⊆ s
x : E
hxs : x ∈ s
hxt : x ∈ ↑(convexHull 𝕜).toOrderHom t
⊢ ↑{ val := x, property := hxs } ∈ ↑(convexHull 𝕜).toOrderHom t
exact hxt
case mpr
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39598
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hc : ∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜).toOrderHom t ⊆ t
t : Set { x // x ∈ s }
x : { x // x ∈ s }
h : ↑x ∈ ↑(convexHull 𝕜).toOrderHom (Subtype.val '' t)
⊢ x ∈ t
case mpr
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39598
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t s : Set E
⊢ (∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜).toOrderHom t ⊆ t) → ConvexIndependent 𝕜 Subtype.val
intro hc t x h
case mpr
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39598
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hc : ∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜).toOrderHom t ⊆ t
t : Set { x // x ∈ s }
x : { x // x ∈ s }
h : ↑x ∈ ↑(convexHull 𝕜).toOrderHom (Subtype.val '' t)
⊢ ↑x ∈ (fun a => ↑a) '' t
case mpr
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39598
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hc : ∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜).toOrderHom t ⊆ t
t : Set { x // x ∈ s }
x : { x // x ∈ s }
h : ↑x ∈ ↑(convexHull 𝕜).toOrderHom (Subtype.val '' t)
⊢ x ∈ t
rw [← Subtype.coe_injective.mem_set_image]
no goals
case mpr
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.39598
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t✝ s : Set E
hc : ∀ (t : Set E), t ⊆ s → s ∩ ↑(convexHull 𝕜).toOrderHom t ⊆ t
t : Set { x // x ∈ s }
x : { x // x ∈ s }
h : ↑x ∈ ↑(convexHull 𝕜).toOrderHom (Subtype.val '' t)
⊢ ↑x ∈ (fun a => ↑a) '' t
exact hc (t.image ((↑) : s → E)) (Subtype.coe_image_subset s t) ⟨x.prop, h⟩