ι : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this : Nonempty (PartialRefinement u s)
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
ι : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
haveI : Nonempty (PartialRefinement u s) := ⟨⟨u, ∅, uo, us, False.elim, fun _ => rfl⟩⟩
case intro
ι : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∀ (a : PartialRefinement u s), v ≤ a → a = v
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
ι : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
rcases zorn_nonempty_partialOrder this with ⟨v, hv⟩
case intro
ι : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝¹ : Nonempty (PartialRefinement u s)
this✝ :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∀ (a : PartialRefinement u s), v ≤ a → a = v
this : ∀ (i : ι), i ∈ v.carrier
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i

case this
ι : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∀ (a : PartialRefinement u s), v ≤ a → a = v
⊢ ∀ (i : ι), i ∈ v.carrier
case intro
ι : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∀ (a : PartialRefinement u s), v ≤ a → a = v
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i
suffices : ∀ i, i ∈ v.carrier
case this
ι : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∀ (a : PartialRefinement u s), v ≤ a → a = v
⊢ ∀ (i : ι), i ∈ v.carrier
case intro
ι : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝¹ : Nonempty (PartialRefinement u s)
this✝ :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∀ (a : PartialRefinement u s), v ≤ a → a = v
this : ∀ (i : ι), i ∈ v.carrier
⊢ ∃ v, s ⊆ iUnion v ∧ (∀ (i : ι), IsOpen (v i)) ∧ ∀ (i : ι), closure (v i) ⊆ u i

case this
ι : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∀ (a : PartialRefinement u s), v ≤ a → a = v
⊢ ∀ (i : ι), i ∈ v.carrier
exact ⟨v, v.subset_iUnion, fun i => v.isOpen _, fun i => v.closure_subset (this i)⟩
case this
ι : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∃ i, ¬i ∈ v.carrier
⊢ ∃ a, v ≤ a ∧ a ≠ v
case this
ι : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∀ (a : PartialRefinement u s), v ≤ a → a = v
⊢ ∀ (i : ι), i ∈ v.carrier
contrapose! hv
case this.intro
ι : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
i : ι
hi : ¬i ∈ v.carrier
⊢ ∃ a, v ≤ a ∧ a ≠ v
case this
ι : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
hv : ∃ i, ¬i ∈ v.carrier
⊢ ∃ a, v ≤ a ∧ a ≠ v
rcases hv with ⟨i, hi⟩
case this.intro.intro
ι : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
i : ι
hi : ¬i ∈ v.carrier
v' : PartialRefinement u s
hlt : v < v'
⊢ ∃ a, v ≤ a ∧ a ≠ v
case this.intro
ι : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
i : ι
hi : ¬i ∈ v.carrier
⊢ ∃ a, v ≤ a ∧ a ≠ v
rcases v.exists_gt hs i hi with ⟨v', hlt⟩
no goals
case this.intro.intro
ι : Type u_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
u : ι → Set X
s : Set X
hs : IsClosed s
uo : ∀ (i : ι), IsOpen (u i)
uf : ∀ (x : X), x ∈ s → Set.Finite {i | x ∈ u i}
us : s ⊆ ⋃ (i : ι), u i
this✝ : Nonempty (PartialRefinement u s)
this :
  ∀ (c : Set (PartialRefinement u s)),
    IsChain (fun x x_1 => x ≤ x_1) c → Set.Nonempty c → ∃ ub, ∀ (v : PartialRefinement u s), v ∈ c → v ≤ ub
v : PartialRefinement u s
i : ι
hi : ¬i ∈ v.carrier
v' : PartialRefinement u s
hlt : v < v'
⊢ ∃ a, v ≤ a ∧ a ≠ v
exact ⟨v', hlt.le, hlt.ne'⟩