case h
α✝ : Type u
β : Type v
ι : Type ?u.184350
π : ι → Type ?u.184355
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s✝ t : Set α✝
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ s ∈ irreducibleComponents α ↔ s ∈ maximals (fun x x_1 => x ≤ x_1) {s | IsClosed s ∧ IsIrreducible s}
α✝ : Type u
β : Type v
ι : Type ?u.184350
π : ι → Type ?u.184355
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s t : Set α✝
α : Type u_1
inst✝ : TopologicalSpace α
⊢ irreducibleComponents α = maximals (fun x x_1 => x ≤ x_1) {s | IsClosed s ∧ IsIrreducible s}
ext s
case h.mp
α✝ : Type u
β : Type v
ι : Type ?u.184350
π : ι → Type ?u.184355
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s✝ t : Set α✝
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ s ∈ irreducibleComponents α → s ∈ maximals (fun x x_1 => x ≤ x_1) {s | IsClosed s ∧ IsIrreducible s}

case h.mpr
α✝ : Type u
β : Type v
ι : Type ?u.184350
π : ι → Type ?u.184355
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s✝ t : Set α✝
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ s ∈ maximals (fun x x_1 => x ≤ x_1) {s | IsClosed s ∧ IsIrreducible s} → s ∈ irreducibleComponents α
case h
α✝ : Type u
β : Type v
ι : Type ?u.184350
π : ι → Type ?u.184355
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s✝ t : Set α✝
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ s ∈ irreducibleComponents α ↔ s ∈ maximals (fun x x_1 => x ≤ x_1) {s | IsClosed s ∧ IsIrreducible s}
constructor
case h.mp
α✝ : Type u
β : Type v
ι : Type ?u.184350
π : ι → Type ?u.184355
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s✝ t : Set α✝
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
H : s ∈ irreducibleComponents α
⊢ s ∈ maximals (fun x x_1 => x ≤ x_1) {s | IsClosed s ∧ IsIrreducible s}
case h.mp
α✝ : Type u
β : Type v
ι : Type ?u.184350
π : ι → Type ?u.184355
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s✝ t : Set α✝
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ s ∈ irreducibleComponents α → s ∈ maximals (fun x x_1 => x ≤ x_1) {s | IsClosed s ∧ IsIrreducible s}
intro H
no goals
case h.mp
α✝ : Type u
β : Type v
ι : Type ?u.184350
π : ι → Type ?u.184355
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s✝ t : Set α✝
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
H : s ∈ irreducibleComponents α
⊢ s ∈ maximals (fun x x_1 => x ≤ x_1) {s | IsClosed s ∧ IsIrreducible s}
exact ⟨⟨isClosed_of_mem_irreducibleComponents _ H, H.1⟩, fun x h e => H.2 h.2 e⟩
case h.mpr
α✝ : Type u
β : Type v
ι : Type ?u.184350
π : ι → Type ?u.184355
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s✝ t : Set α✝
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
H : s ∈ maximals (fun x x_1 => x ≤ x_1) {s | IsClosed s ∧ IsIrreducible s}
⊢ s ∈ irreducibleComponents α
case h.mpr
α✝ : Type u
β : Type v
ι : Type ?u.184350
π : ι → Type ?u.184355
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s✝ t : Set α✝
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
⊢ s ∈ maximals (fun x x_1 => x ≤ x_1) {s | IsClosed s ∧ IsIrreducible s} → s ∈ irreducibleComponents α
intro H
case h.mpr
α✝ : Type u
β : Type v
ι : Type ?u.184350
π : ι → Type ?u.184355
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s✝ t : Set α✝
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
H : s ∈ maximals (fun x x_1 => x ≤ x_1) {s | IsClosed s ∧ IsIrreducible s}
x : Set α
h : x ∈ {s | IsIrreducible s}
e : (fun x x_1 => x ≤ x_1) s x
⊢ (fun x x_1 => x ≤ x_1) x s
case h.mpr
α✝ : Type u
β : Type v
ι : Type ?u.184350
π : ι → Type ?u.184355
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s✝ t : Set α✝
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
H : s ∈ maximals (fun x x_1 => x ≤ x_1) {s | IsClosed s ∧ IsIrreducible s}
⊢ s ∈ irreducibleComponents α
refine' ⟨H.1.2, fun x h e => _⟩
case h.mpr
α✝ : Type u
β : Type v
ι : Type ?u.184350
π : ι → Type ?u.184355
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s✝ t : Set α✝
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
H : s ∈ maximals (fun x x_1 => x ≤ x_1) {s | IsClosed s ∧ IsIrreducible s}
x : Set α
h : x ∈ {s | IsIrreducible s}
e : (fun x x_1 => x ≤ x_1) s x
this : closure x ≤ s
⊢ (fun x x_1 => x ≤ x_1) x s
case h.mpr
α✝ : Type u
β : Type v
ι : Type ?u.184350
π : ι → Type ?u.184355
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s✝ t : Set α✝
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
H : s ∈ maximals (fun x x_1 => x ≤ x_1) {s | IsClosed s ∧ IsIrreducible s}
x : Set α
h : x ∈ {s | IsIrreducible s}
e : (fun x x_1 => x ≤ x_1) s x
⊢ (fun x x_1 => x ≤ x_1) x s
have : closure x ≤ s := H.2 ⟨isClosed_closure, h.closure⟩ (e.trans subset_closure)
no goals
case h.mpr
α✝ : Type u
β : Type v
ι : Type ?u.184350
π : ι → Type ?u.184355
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s✝ t : Set α✝
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
H : s ∈ maximals (fun x x_1 => x ≤ x_1) {s | IsClosed s ∧ IsIrreducible s}
x : Set α
h : x ∈ {s | IsIrreducible s}
e : (fun x x_1 => x ≤ x_1) s x
this : closure x ≤ s
⊢ (fun x x_1 => x ≤ x_1) x s
exact le_trans subset_closure this