𝕜 : Type u_2
E : Type u_3
ι : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s✝ t : Set E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
⊢ x ∈ s
𝕜 : Type u_2
E : Type u_3
ι : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s t : Set E
inst✝ : Subsingleton ι
p : ι → E
⊢ ConvexIndependent 𝕜 p
intro s x hx
𝕜 : Type u_2
E : Type u_3
ι : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s✝ t : Set E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
this : Set.Nonempty (↑(convexHull 𝕜).toOrderHom (p '' s))
⊢ x ∈ s
𝕜 : Type u_2
E : Type u_3
ι : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s✝ t : Set E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
⊢ x ∈ s
have : (convexHull 𝕜 (p '' s)).Nonempty := ⟨p x, hx⟩
𝕜 : Type u_2
E : Type u_3
ι : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s✝ t : Set E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
this : Set.Nonempty s
⊢ x ∈ s
𝕜 : Type u_2
E : Type u_3
ι : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s✝ t : Set E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
this : Set.Nonempty (↑(convexHull 𝕜).toOrderHom (p '' s))
⊢ x ∈ s
rw [convexHull_nonempty_iff, Set.nonempty_image_iff] at this
no goals
𝕜 : Type u_2
E : Type u_3
ι : Type u_1
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
s✝ t : Set E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : p x ∈ ↑(convexHull 𝕜).toOrderHom (p '' s)
this : Set.Nonempty s
⊢ x ∈ s
rwa [Subsingleton.mem_iff_nonempty]