by_cases hxspace : x ∈ K.space
case mp.intro
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
⊢ ∃ s ∈ K.faces, s.Nonempty ∧ ¬K.LocallyFiniteAt s
case pos
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∈ K.space
⊢ ∃ s ∈ K.faces, s.Nonempty ∧ ¬K.LocallyFiniteAt s

case neg
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
K K₁ K₂ : SimplicialComplex 𝕜 E
x✝ t✝ : E
s t : Finset E
A : Set (Finset E)
m n : ℕ
inst✝ : DecidableEq E
x : E
hx : ¬{s | s ∈ K.faces ∧ x ∈ (convexHull 𝕜) ↑s}.Finite
hxspace : x ∉ K.space
⊢ ∃ s ∈ K.faces, s.Nonempty ∧ ¬K.LocallyFiniteAt s