𝕜 : Type u_2
E : Type u_1
ι : Type ?u.42000
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
h : x ∈ ↑(convexHull 𝕜).toOrderHom ↑s
⊢ x ∈ s
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.42000
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
⊢ x ∈ ↑(convexHull 𝕜).toOrderHom ↑s ↔ x ∈ s
refine' ⟨fun h => _, fun h => subset_convexHull 𝕜 _ h⟩
no goals
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.42000
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
h : x ∈ ↑(convexHull 𝕜).toOrderHom ↑s
⊢ x ∈ s
classical
have h := K.inter_subset_convexHull hx hs ⟨by simp, h⟩
by_contra H
rwa [← coe_inter, Finset.disjoint_iff_inter_eq_empty.1 (Finset.disjoint_singleton_right.2 H).symm,
  coe_empty, convexHull_empty] at h
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.42000
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
h✝ : x ∈ ↑(convexHull 𝕜).toOrderHom ↑s
h : x ∈ ↑(convexHull 𝕜).toOrderHom (↑{x} ∩ ↑s)
⊢ x ∈ s
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.42000
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
h : x ∈ ↑(convexHull 𝕜).toOrderHom ↑s
⊢ x ∈ s
have h := K.inter_subset_convexHull hx hs ⟨by simp, h⟩
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.42000
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
h✝ : x ∈ ↑(convexHull 𝕜).toOrderHom ↑s
h : x ∈ ↑(convexHull 𝕜).toOrderHom (↑{x} ∩ ↑s)
H : ¬x ∈ s
⊢ False
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.42000
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
h✝ : x ∈ ↑(convexHull 𝕜).toOrderHom ↑s
h : x ∈ ↑(convexHull 𝕜).toOrderHom (↑{x} ∩ ↑s)
⊢ x ∈ s
by_contra H
no goals
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.42000
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
h✝ : x ∈ ↑(convexHull 𝕜).toOrderHom ↑s
h : x ∈ ↑(convexHull 𝕜).toOrderHom (↑{x} ∩ ↑s)
H : ¬x ∈ s
⊢ False
rwa [← coe_inter, Finset.disjoint_iff_inter_eq_empty.1 (Finset.disjoint_singleton_right.2 H).symm,
  coe_empty, convexHull_empty] at h
no goals
𝕜 : Type u_2
E : Type u_1
ι : Type ?u.42000
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
K : SimplicialComplex 𝕜 E
s t : Finset E
x : E
hx : x ∈ vertices K
hs : s ∈ K.faces
h : x ∈ ↑(convexHull 𝕜).toOrderHom ↑s
⊢ x ∈ ↑(convexHull 𝕜).toOrderHom ↑{x}
simp