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

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t : Finset E
inst✝ : FiniteDimensional ℝ E
hs : AffineIndependent ℝ Subtype.val
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
⊢ combiInterior ℝ s = interior ((convexHull ℝ) ↑s)
Tactic:
unfold combiInterior
State after:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t : Finset E
inst✝ : FiniteDimensional ℝ E
hs : AffineIndependent ℝ Subtype.val
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
⊢ (convexHull ℝ) ↑s \ combiFrontier ℝ s = interior ((convexHull ℝ) ↑s)

State before:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module ℝ E
inst✝³ : TopologicalAddGroup E
inst✝² : ContinuousSMul ℝ E
inst✝¹ : T2Space E
s t : Finset E
inst✝ : FiniteDimensional ℝ E
hs : AffineIndependent ℝ Subtype.val
hscard : s.card = FiniteDimensional.finrank ℝ E + 1
⊢ (convexHull ℝ) ↑s \ combiFrontier ℝ s = interior ((convexHull ℝ) ↑s)
Tactic:
sorry
State after:
no goals