Theorem: isClosed_combiFrontier (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
⊢ IsClosed (combiFrontier ℝ s)
Tactic:
refine' Set.Finite.isClosed_biUnion _ fun t _ => t.isClosed_convexHull
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
⊢ Set.Finite fun t => t ⊆ s ∧ ¬s ⊆ t

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
⊢ Set.Finite fun t => t ⊆ s ∧ ¬s ⊆ t
Tactic:
suffices Set.Finite {t | t ⊆ s} by exact this.subset fun i h => h.1
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
⊢ {t | t ⊆ s}.Finite

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
⊢ {t | t ⊆ s}.Finite
Tactic:
convert s.powerset.finite_toSet using 1
State after:
case h.e'_2
𝕜 : 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
⊢ {t | t ⊆ s} = ↑s.powerset

State before:
case h.e'_2
𝕜 : 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
⊢ {t | t ⊆ s} = ↑s.powerset
Tactic:
ext
State after:
case h.e'_2.h
𝕜 : 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 x✝ : Finset E
⊢ x✝ ∈ {t | t ⊆ s} ↔ x✝ ∈ ↑s.powerset

State before:
case h.e'_2.h
𝕜 : 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 x✝ : Finset E
⊢ x✝ ∈ {t | t ⊆ s} ↔ x✝ ∈ ↑s.powerset
Tactic:
simp
State after:
no goals

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
this : {t | t ⊆ s}.Finite
⊢ Set.Finite fun t => t ⊆ s ∧ ¬s ⊆ t
Tactic:
exact this.subset fun i h => h.1
State after:
no goals