Theorem: AffineIndependent.convexIndependent (LeanCamCombi/Mathlib/Analysis/Convex/Independence.lean)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hp : AffineIndependent 𝕜 p
⊢ ConvexIndependent 𝕜 p
Tactic:
intro s x hx
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hp : AffineIndependent 𝕜 p
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
⊢ x ∈ s

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hp : AffineIndependent 𝕜 p
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
⊢ x ∈ s
Tactic:
by_contra
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hp : AffineIndependent 𝕜 p
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
x✝ : x ∉ s
⊢ False

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : ι → E
hp : AffineIndependent 𝕜 p
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
x✝ : x ∉ s
⊢ False
Tactic:
sorry
State after:
no goals