Theorem: combiFrontier_empty (LeanCamCombi/SimplicialComplex/Simplex.lean)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ combiFrontier 𝕜 ∅ = ∅
Tactic:
apply Set.eq_empty_of_subset_empty
State after:
case a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ combiFrontier 𝕜 ∅ ⊆ ∅

State before:
case a
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ combiFrontier 𝕜 ∅ ⊆ ∅
Tactic:
convert combiFrontier_subset_convexHull
State after:
case h.e'_4
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ ∅ = (convexHull 𝕜) ↑∅

State before:
case h.e'_4
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : OrderedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s t : Finset E
x : E
⊢ ∅ = (convexHull 𝕜) ↑∅
Tactic:
rw [Finset.coe_empty, convexHull_empty]
State after:
no goals