Theorem: convexHull_subset_convexHull_of_combiInterior_subset_combiInterior (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
ht : AffineIndependent ℝ Subtype.val
⊢ combiInterior ℝ s ⊆ combiInterior ℝ t → (convexHull ℝ) ↑s ⊆ (convexHull ℝ) ↑t
Tactic:
rw [← closure_combiInterior_eq_convexHull hs]
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
ht : AffineIndependent ℝ Subtype.val
⊢ combiInterior ℝ s ⊆ combiInterior ℝ t → closure (combiInterior ℝ s) ⊆ (convexHull ℝ) ↑t

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
ht : AffineIndependent ℝ Subtype.val
⊢ combiInterior ℝ s ⊆ combiInterior ℝ t → closure (combiInterior ℝ s) ⊆ (convexHull ℝ) ↑t
Tactic:
rw [← closure_combiInterior_eq_convexHull ht]
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
ht : AffineIndependent ℝ Subtype.val
⊢ combiInterior ℝ s ⊆ combiInterior ℝ t → closure (combiInterior ℝ s) ⊆ closure (combiInterior ℝ t)

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
ht : AffineIndependent ℝ Subtype.val
⊢ combiInterior ℝ s ⊆ combiInterior ℝ t → closure (combiInterior ℝ s) ⊆ closure (combiInterior ℝ t)
Tactic:
intro h
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
ht : AffineIndependent ℝ Subtype.val
h : combiInterior ℝ s ⊆ combiInterior ℝ t
⊢ closure (combiInterior ℝ s) ⊆ closure (combiInterior ℝ t)

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
ht : AffineIndependent ℝ Subtype.val
h : combiInterior ℝ s ⊆ combiInterior ℝ t
⊢ closure (combiInterior ℝ s) ⊆ closure (combiInterior ℝ t)
Tactic:
apply closure_mono h
State after:
no goals