case intro.intro.intro.intro
α : Type u_1
β : Type ?u.25119
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
S : Set (Set α)
hSf : Set.Finite S
hSc : ∀ (t : Set α), t ∈ S → IsClosed t
hSi : ∀ (t : Set α), t ∈ S → IsIrreducible t
hSU : Set.univ = ⋃₀ S
⊢ Set.Finite (irreducibleComponents α)
α : Type u_1
β : Type ?u.25119
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
⊢ Set.Finite (irreducibleComponents α)
obtain ⟨S : Set (Set α), hSf, hSc, hSi, hSU⟩ :=
  NoetherianSpace.exists_finite_set_isClosed_irreducible isClosed_univ
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.25119
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
S : Set (Set α)
hSf : Set.Finite S
hSc : ∀ (t : Set α), t ∈ S → IsClosed t
hSi : ∀ (t : Set α), t ∈ S → IsIrreducible t
hSU : Set.univ = ⋃₀ S
s : Set α
hs : s ∈ irreducibleComponents α
⊢ s ∈ S
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.25119
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
S : Set (Set α)
hSf : Set.Finite S
hSc : ∀ (t : Set α), t ∈ S → IsClosed t
hSi : ∀ (t : Set α), t ∈ S → IsIrreducible t
hSU : Set.univ = ⋃₀ S
⊢ Set.Finite (irreducibleComponents α)
refine hSf.subset fun s hs => ?_
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.25119
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Set α
hs : s ∈ irreducibleComponents α
S : Finset (Set α)
hSc : ∀ (t : Set α), t ∈ ↑S → IsClosed t
hSi : ∀ (t : Set α), t ∈ ↑S → IsIrreducible t
hSU : Set.univ = ⋃₀ ↑S
⊢ s ∈ ↑S
case intro.intro.intro.intro
α : Type u_1
β : Type ?u.25119
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
S : Set (Set α)
hSf : Set.Finite S
hSc : ∀ (t : Set α), t ∈ S → IsClosed t
hSi : ∀ (t : Set α), t ∈ S → IsIrreducible t
hSU : Set.univ = ⋃₀ S
s : Set α
hs : s ∈ irreducibleComponents α
⊢ s ∈ S
lift S to Finset (Set α) using hSf
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.25119
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Set α
hs : s ∈ irreducibleComponents α
S : Finset (Set α)
hSc : ∀ (t : Set α), t ∈ ↑S → IsClosed t
hSi : ∀ (t : Set α), t ∈ ↑S → IsIrreducible t
hSU : Set.univ = ⋃₀ ↑S
t : Set α
htS : t ∈ S
ht : s ⊆ t
⊢ s ∈ ↑S
case intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.25119
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Set α
hs : s ∈ irreducibleComponents α
S : Finset (Set α)
hSc : ∀ (t : Set α), t ∈ ↑S → IsClosed t
hSi : ∀ (t : Set α), t ∈ ↑S → IsIrreducible t
hSU : Set.univ = ⋃₀ ↑S
⊢ s ∈ ↑S
rcases isIrreducible_iff_sUnion_closed.1 hs.1 S hSc (hSU ▸ Set.subset_univ _) with ⟨t, htS, ht⟩
no goals
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type ?u.25119
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : NoetherianSpace α
s : Set α
hs : s ∈ irreducibleComponents α
S : Finset (Set α)
hSc : ∀ (t : Set α), t ∈ ↑S → IsClosed t
hSi : ∀ (t : Set α), t ∈ ↑S → IsIrreducible t
hSU : Set.univ = ⋃₀ ↑S
t : Set α
htS : t ∈ S
ht : s ⊆ t
⊢ s ∈ ↑S
rwa [ht.antisymm (hs.2 (hSi _ htS) ht)]