α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ connectedComponent x
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
⊢ connectedComponent x = ⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z
apply Subset.antisymm connectedComponent_subset_iInter_clopen
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
⊢ IsPreconnected (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ connectedComponent x
refine' IsPreconnected.subset_connectedComponent _ (mem_iInter.2 fun Z => Z.2.2)
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
⊢ IsPreconnected (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
⊢ IsPreconnected (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
have hs : @IsClosed α _ (⋂ Z : { Z : Set α // IsClopen Z ∧ x ∈ Z }, Z) :=
  isClosed_iInter fun Z => Z.2.1.2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
⊢ ∀ (u v : Set α),
    IsClosed u →
      IsClosed v →
        (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ u ∪ v →
          Disjoint u v → (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ u ∨ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ v
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
⊢ IsPreconnected (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
rw [isPreconnected_iff_subset_of_fully_disjoint_closed hs]
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∨ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ b
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
⊢ ∀ (u v : Set α),
    IsClosed u →
      IsClosed v →
        (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ u ∪ v →
          Disjoint u v → (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ u ∨ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ v
intro a b ha hb hab ab_disj
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∨ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ b
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∨ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ b
haveI := @normalOfCompactT2 α _ _ _
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∨ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ b
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∨ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ b
rcases normal_separation ha hb ab_disj with ⟨u, v, hu, hv, hau, hbv, huv⟩
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
⊢ ∃ Z, IsClopen Z ∧ x ∈ Z ∧ Z ⊆ u ∪ v

case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ u ∪ v
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∨ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ b
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∨ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ b
obtain ⟨Z, H⟩ : ∃ Z : Set α, IsClopen Z ∧ x ∈ Z ∧ Z ⊆ u ∪ v
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 :
  (∀ (t : Finset { Z // IsClopen Z ∧ x ∈ Z }),
      Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ t), (fun Z => ↑Z) i)) →
    Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }), (fun Z => ↑Z) i)
⊢ ∃ Z, IsClopen Z ∧ x ∈ Z ∧ Z ⊆ u ∪ v
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
⊢ ∃ Z, IsClopen Z ∧ x ∈ Z ∧ Z ⊆ u ∪ v
have H1 := (hu.union hv).isClosed_compl.isCompact.inter_iInter_nonempty
  (fun Z : { Z : Set α // IsClopen Z ∧ x ∈ Z } => Z) fun Z => Z.2.1.2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 :
  Disjoint ((u ∪ v)ᶜ) (⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }), (fun Z => ↑Z) i) →
    ∃ x_1, ¬Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ x_1), (fun Z => ↑Z) i)
⊢ ∃ Z, IsClopen Z ∧ x ∈ Z ∧ Z ⊆ u ∪ v
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 :
  (∀ (t : Finset { Z // IsClopen Z ∧ x ∈ Z }),
      Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ t), (fun Z => ↑Z) i)) →
    Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }), (fun Z => ↑Z) i)
⊢ ∃ Z, IsClopen Z ∧ x ∈ Z ∧ Z ⊆ u ∪ v
rw [← not_disjoint_iff_nonempty_inter, imp_not_comm, not_forall] at H1
case intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 :
  Disjoint ((u ∪ v)ᶜ) (⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }), (fun Z => ↑Z) i) →
    ∃ x_1, ¬Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ x_1), (fun Z => ↑Z) i)
Zi : Finset { Z // IsClopen Z ∧ x ∈ Z }
H2 : ¬Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ Zi), (fun Z => ↑Z) i)
⊢ ∃ Z, IsClopen Z ∧ x ∈ Z ∧ Z ⊆ u ∪ v
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 :
  Disjoint ((u ∪ v)ᶜ) (⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }), (fun Z => ↑Z) i) →
    ∃ x_1, ¬Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ x_1), (fun Z => ↑Z) i)
⊢ ∃ Z, IsClopen Z ∧ x ∈ Z ∧ Z ⊆ u ∪ v
cases' H1 (disjoint_compl_left_iff_subset.2 <| hab.trans <| union_subset_union hau hbv)
  with Zi H2
case intro.refine'_1
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 :
  Disjoint ((u ∪ v)ᶜ) (⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }), (fun Z => ↑Z) i) →
    ∃ x_1, ¬Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ x_1), (fun Z => ↑Z) i)
Zi : Finset { Z // IsClopen Z ∧ x ∈ Z }
H2 : ¬Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ Zi), (fun Z => ↑Z) i)
⊢ IsClopen (⋂ (U : { Z // IsClopen Z ∧ x ∈ Z }) (_ : U ∈ Zi), ↑U)

case intro.refine'_2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 :
  Disjoint ((u ∪ v)ᶜ) (⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }), (fun Z => ↑Z) i) →
    ∃ x_1, ¬Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ x_1), (fun Z => ↑Z) i)
Zi : Finset { Z // IsClopen Z ∧ x ∈ Z }
H2 : ¬Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ Zi), (fun Z => ↑Z) i)
⊢ x ∈ ⋂ (U : { Z // IsClopen Z ∧ x ∈ Z }) (_ : U ∈ Zi), ↑U

case intro.refine'_3
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 :
  Disjoint ((u ∪ v)ᶜ) (⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }), (fun Z => ↑Z) i) →
    ∃ x_1, ¬Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ x_1), (fun Z => ↑Z) i)
Zi : Finset { Z // IsClopen Z ∧ x ∈ Z }
H2 : ¬Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ Zi), (fun Z => ↑Z) i)
⊢ (⋂ (U : { Z // IsClopen Z ∧ x ∈ Z }) (_ : U ∈ Zi), ↑U) ⊆ u ∪ v
case intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 :
  Disjoint ((u ∪ v)ᶜ) (⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }), (fun Z => ↑Z) i) →
    ∃ x_1, ¬Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ x_1), (fun Z => ↑Z) i)
Zi : Finset { Z // IsClopen Z ∧ x ∈ Z }
H2 : ¬Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ Zi), (fun Z => ↑Z) i)
⊢ ∃ Z, IsClopen Z ∧ x ∈ Z ∧ Z ⊆ u ∪ v
refine' ⟨⋂ U ∈ Zi, Subtype.val U, _, _, _⟩
no goals
case intro.refine'_1
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 :
  Disjoint ((u ∪ v)ᶜ) (⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }), (fun Z => ↑Z) i) →
    ∃ x_1, ¬Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ x_1), (fun Z => ↑Z) i)
Zi : Finset { Z // IsClopen Z ∧ x ∈ Z }
H2 : ¬Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ Zi), (fun Z => ↑Z) i)
⊢ IsClopen (⋂ (U : { Z // IsClopen Z ∧ x ∈ Z }) (_ : U ∈ Zi), ↑U)
exact isClopen_biInter_finset fun Z _ => Z.2.1
no goals
case intro.refine'_2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 :
  Disjoint ((u ∪ v)ᶜ) (⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }), (fun Z => ↑Z) i) →
    ∃ x_1, ¬Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ x_1), (fun Z => ↑Z) i)
Zi : Finset { Z // IsClopen Z ∧ x ∈ Z }
H2 : ¬Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ Zi), (fun Z => ↑Z) i)
⊢ x ∈ ⋂ (U : { Z // IsClopen Z ∧ x ∈ Z }) (_ : U ∈ Zi), ↑U
exact mem_iInter₂.2 fun Z _ => Z.2.2
no goals
case intro.refine'_3
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
H1 :
  Disjoint ((u ∪ v)ᶜ) (⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }), (fun Z => ↑Z) i) →
    ∃ x_1, ¬Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ x_1), (fun Z => ↑Z) i)
Zi : Finset { Z // IsClopen Z ∧ x ∈ Z }
H2 : ¬Set.Nonempty ((u ∪ v)ᶜ ∩ ⋂ (i : { Z // IsClopen Z ∧ x ∈ Z }) (_ : i ∈ Zi), (fun Z => ↑Z) i)
⊢ (⋂ (U : { Z // IsClopen Z ∧ x ∈ Z }) (_ : U ∈ Zi), ↑U) ⊆ u ∪ v
rwa [← disjoint_compl_left_iff_subset, disjoint_iff_inter_eq_empty,
  ← not_nonempty_iff_eq_empty]
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ u ∪ v
H1 : IsClopen (Z ∩ u)
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∨ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ b
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ u ∪ v
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∨ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ b
have H1 := isClopen_inter_of_disjoint_cover_clopen H.1 H.2.2 hu hv huv
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ v ∪ u
H1 : IsClopen (Z ∩ u)
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∨ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ b
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ u ∪ v
H1 : IsClopen (Z ∩ u)
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∨ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ b
rw [union_comm] at H
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ v ∪ u
H1 : IsClopen (Z ∩ u)
H2 : IsClopen (Z ∩ v)
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∨ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ b
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ v ∪ u
H1 : IsClopen (Z ∩ u)
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∨ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ b
have H2 := isClopen_inter_of_disjoint_cover_clopen H.1 H.2.2 hv hu huv.symm
case pos.h
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ v ∪ u
H1 : IsClopen (Z ∩ u)
H2 : IsClopen (Z ∩ v)
hxu : x ∈ u
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a

case neg.h
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ v ∪ u
H1 : IsClopen (Z ∩ u)
H2 : IsClopen (Z ∩ v)
hxu : ¬x ∈ u
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ b
case intro.intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ v ∪ u
H1 : IsClopen (Z ∩ u)
H2 : IsClopen (Z ∩ v)
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∨ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ b
by_cases hxu : x ∈ u <;> [left; right]
case pos.h
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ v ∪ u
H1 : IsClopen (Z ∩ u)
H2 : IsClopen (Z ∩ v)
hxu : x ∈ u
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ u
case pos.h
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ v ∪ u
H1 : IsClopen (Z ∩ u)
H2 : IsClopen (Z ∩ v)
hxu : x ∈ u
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a
suffices (⋂ Z : { Z : Set α // IsClopen Z ∧ x ∈ Z }, ↑Z) ⊆ u
  from Disjoint.left_le_of_le_sup_right hab (huv.mono this hbv)
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ v ∪ u
H1 : IsClopen (Z ∩ u)
H2 : IsClopen (Z ∩ v)
hxu : x ∈ u
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ Z ∩ u
case pos.h
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ v ∪ u
H1 : IsClopen (Z ∩ u)
H2 : IsClopen (Z ∩ v)
hxu : x ∈ u
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ u
apply Subset.trans _ (inter_subset_right Z u)
no goals
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ v ∪ u
H1 : IsClopen (Z ∩ u)
H2 : IsClopen (Z ∩ v)
hxu : x ∈ u
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ Z ∩ u
exact iInter_subset (fun Z : { Z : Set α // IsClopen Z ∧ x ∈ Z } => Z.1)
  ⟨Z ∩ u, H1, mem_inter H.2.1 hxu⟩
case neg.h
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ v ∪ u
H1 : IsClopen (Z ∩ u)
H2 : IsClopen (Z ∩ v)
hxu : ¬x ∈ u
h1 : x ∈ v
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ b
case neg.h
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ v ∪ u
H1 : IsClopen (Z ∩ u)
H2 : IsClopen (Z ∩ v)
hxu : ¬x ∈ u
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ b
have h1 : x ∈ v :=
  (hab.trans (union_subset_union hau hbv) (mem_iInter.2 fun i => i.2.2)).resolve_left hxu
case neg.h
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ v ∪ u
H1 : IsClopen (Z ∩ u)
H2 : IsClopen (Z ∩ v)
hxu : ¬x ∈ u
h1 : x ∈ v
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ v
case neg.h
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ v ∪ u
H1 : IsClopen (Z ∩ u)
H2 : IsClopen (Z ∩ v)
hxu : ¬x ∈ u
h1 : x ∈ v
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ b
suffices (⋂ Z : { Z : Set α // IsClopen Z ∧ x ∈ Z }, ↑Z) ⊆ v
  from (huv.symm.mono this hau).left_le_of_le_sup_left hab
case neg.h
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ v ∪ u
H1 : IsClopen (Z ∩ u)
H2 : IsClopen (Z ∩ v)
hxu : ¬x ∈ u
h1 : x ∈ v
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ Z ∩ v
case neg.h
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ v ∪ u
H1 : IsClopen (Z ∩ u)
H2 : IsClopen (Z ∩ v)
hxu : ¬x ∈ u
h1 : x ∈ v
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ v
refine Subset.trans ?_ (inter_subset_right Z v)
no goals
case neg.h
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : T2Space α
inst✝ : CompactSpace α
x : α
hs : IsClosed (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z)
a b : Set α
ha : IsClosed a
hb : IsClosed b
hab : (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ a ∪ b
ab_disj : Disjoint a b
this : NormalSpace α
u v : Set α
hu : IsOpen u
hv : IsOpen v
hau : a ⊆ u
hbv : b ⊆ v
huv : Disjoint u v
Z : Set α
H : IsClopen Z ∧ x ∈ Z ∧ Z ⊆ v ∪ u
H1 : IsClopen (Z ∩ u)
H2 : IsClopen (Z ∩ v)
hxu : ¬x ∈ u
h1 : x ∈ v
⊢ (⋂ (Z : { Z // IsClopen Z ∧ x ∈ Z }), ↑Z) ⊆ Z ∩ v
exact iInter_subset (fun Z : { Z : Set α // IsClopen Z ∧ x ∈ Z } => Z.1)
  ⟨Z ∩ v, H2, mem_inter H.2.1 h1⟩