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

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
⊢ closure (combiInterior ℝ s) = (convexHull ℝ) ↑s
Tactic:
refine'
  Set.Subset.antisymm _
    (convexHull_min (subset_closure_combiInterior hs) (convex_combiInterior hs).closure)
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
⊢ closure (combiInterior ℝ s) ⊆ (convexHull ℝ) ↑s

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
⊢ closure (combiInterior ℝ s) ⊆ (convexHull ℝ) ↑s
Tactic:
rw [s.isClosed_convexHull.closure_subset_iff]
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
⊢ combiInterior ℝ s ⊆ (convexHull ℝ) ↑s

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝² : SeminormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
s t : Finset E
inst✝ : T2Space E
hs : AffineIndependent ℝ Subtype.val
⊢ combiInterior ℝ s ⊆ (convexHull ℝ) ↑s
Tactic:
exact combiInterior_subset_convexHull
State after:
no goals