𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
i j : ι
hij : p i = p j
⊢ p i ∈ ↑(convexHull 𝕜).toOrderHom (p '' {j})
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
⊢ Injective p
refine' fun i j hij => hc {j} i _
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
i j : ι
hij : p i = p j
⊢ p j ∈ {p j}
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
i j : ι
hij : p i = p j
⊢ p i ∈ ↑(convexHull 𝕜).toOrderHom (p '' {j})
rw [hij, Set.image_singleton, convexHull_singleton]
no goals
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
p : ι → E
hc : ConvexIndependent 𝕜 p
i j : ι
hij : p i = p j
⊢ p j ∈ {p j}
exact Set.mem_singleton _