𝕜 : Type u_3
E : Type u_4
ι : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Set E
ι' : Type u_1
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx : (p ∘ ↑f) x ∈ ↑(convexHull 𝕜).toOrderHom (p ∘ ↑f '' s)
⊢ x ∈ s
𝕜 : Type u_3
E : Type u_4
ι : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Set E
ι' : Type u_1
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
⊢ ConvexIndependent 𝕜 (p ∘ ↑f)
intro s x hx
𝕜 : Type u_3
E : Type u_4
ι : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Set E
ι' : Type u_1
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx : (p ∘ ↑f) x ∈ ↑(convexHull 𝕜).toOrderHom (p ∘ ↑f '' s)
⊢ ↑f x ∈ ↑f '' s
𝕜 : Type u_3
E : Type u_4
ι : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Set E
ι' : Type u_1
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx : (p ∘ ↑f) x ∈ ↑(convexHull 𝕜).toOrderHom (p ∘ ↑f '' s)
⊢ x ∈ s
rw [← f.injective.mem_set_image]
no goals
𝕜 : Type u_3
E : Type u_4
ι : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Set E
ι' : Type u_1
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx : (p ∘ ↑f) x ∈ ↑(convexHull 𝕜).toOrderHom (p ∘ ↑f '' s)
⊢ ↑f x ∈ ↑f '' s
exact hc _ _ (by rwa [Set.image_image])
no goals
𝕜 : Type u_3
E : Type u_4
ι : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s✝ t : Set E
ι' : Type u_1
f : ι' ↪ ι
p : ι → E
hc : ConvexIndependent 𝕜 p
s : Set ι'
x : ι'
hx : (p ∘ ↑f) x ∈ ↑(convexHull 𝕜).toOrderHom (p ∘ ↑f '' s)
⊢ p (↑f x) ∈ ↑(convexHull 𝕜).toOrderHom (p '' (↑f '' s))
rwa [Set.image_image]