case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
⊢ ∃ V D, Set.Countable V ∧ Perfect D ∧ C = V ∪ D
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
⊢ ∃ V D, Set.Countable V ∧ Perfect D ∧ C = V ∪ D
obtain ⟨b, bct, _, bbasis⟩ := TopologicalSpace.exists_countable_basis α
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
⊢ ∃ V D, Set.Countable V ∧ Perfect D ∧ C = V ∪ D
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
⊢ ∃ V D, Set.Countable V ∧ Perfect D ∧ C = V ∪ D
let v := { U ∈ b | (U ∩ C).Countable }
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
⊢ ∃ V D, Set.Countable V ∧ Perfect D ∧ C = V ∪ D
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
⊢ ∃ V D, Set.Countable V ∧ Perfect D ∧ C = V ∪ D
let V := ⋃ U ∈ v, U
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
⊢ ∃ V D, Set.Countable V ∧ Perfect D ∧ C = V ∪ D
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
⊢ ∃ V D, Set.Countable V ∧ Perfect D ∧ C = V ∪ D
let D := C \ V
case intro.intro.intro.refine'_1
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
⊢ IsClosed D

case intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
⊢ Preperfect D

case intro.intro.intro.refine'_3
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
⊢ C = V ∩ C ∪ D
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
⊢ ∃ V D, Set.Countable V ∧ Perfect D ∧ C = V ∪ D
refine' ⟨V ∩ C, D, Vct, ⟨_, _⟩, _⟩
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
⊢ Set.Countable (⋃ (i : Set α) (_ : i ∈ b ∧ Set.Countable (i ∩ C)), i ∩ C)
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
⊢ Set.Countable (V ∩ C)
simp only [iUnion_inter, mem_sep_iff]
case hs
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
⊢ Set.Countable fun a => a ∈ b ∧ Set.Countable (a ∩ C)

case a
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
⊢ ∀ (a : Set α), (a ∈ fun a => a ∈ b ∧ Set.Countable (a ∩ C)) → Set.Countable (a ∩ C)
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
⊢ Set.Countable (⋃ (i : Set α) (_ : i ∈ b ∧ Set.Countable (i ∩ C)), i ∩ C)
apply Countable.biUnion
no goals
case hs
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
⊢ Set.Countable fun a => a ∈ b ∧ Set.Countable (a ∩ C)
exact Countable.mono (inter_subset_left _ _) bct
no goals
case a
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
⊢ ∀ (a : Set α), (a ∈ fun a => a ∈ b ∧ Set.Countable (a ∩ C)) → Set.Countable (a ∩ C)
exact inter_subset_right _ _
case intro.intro.intro.refine'_1
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x✝ : Set α
⊢ x✝ ∈ v → IsOpen x✝
case intro.intro.intro.refine'_1
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
⊢ IsClosed D
refine' hclosed.sdiff (isOpen_biUnion fun _ ↦ _)
no goals
case intro.intro.intro.refine'_1
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x✝ : Set α
⊢ x✝ ∈ v → IsOpen x✝
exact fun ⟨Ub, _⟩ ↦ IsTopologicalBasis.isOpen bbasis Ub
case intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
⊢ ∀ (x : α), x ∈ D → ∀ (U : Set α), U ∈ 𝓝 x → ∃ y, y ∈ U ∩ D ∧ y ≠ x
case intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
⊢ Preperfect D
rw [preperfect_iff_nhds]
case intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
⊢ ∃ y, y ∈ E ∩ D ∧ y ≠ x
case intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
⊢ ∀ (x : α), x ∈ D → ∀ (U : Set α), U ∈ 𝓝 x → ∃ y, y ∈ U ∩ D ∧ y ≠ x
intro x xD E xE
case intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
this : ¬Set.Countable (E ∩ D)
h : ¬∃ y, y ∈ E ∩ D ∧ y ≠ x
⊢ False
case intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
this : ¬Set.Countable (E ∩ D)
⊢ ∃ y, y ∈ E ∩ D ∧ y ≠ x
by_contra h
case intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
this : ¬Set.Countable (E ∩ D)
h : ∀ (x_1 : α), ¬(x_1 ∈ E ∩ D ∧ x_1 ≠ x)
⊢ False
case intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
this : ¬Set.Countable (E ∩ D)
h : ¬∃ y, y ∈ E ∩ D ∧ y ≠ x
⊢ False
rw [not_exists] at h
case intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
this : ¬Set.Countable (E ∩ D)
h : ∀ (x_1 : α), x_1 ∈ E ∩ (C \ V) → x_1 = x
⊢ False
case intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
this : ¬Set.Countable (E ∩ D)
h : ∀ (x_1 : α), ¬(x_1 ∈ E ∩ D ∧ x_1 ≠ x)
⊢ False
push_neg at h
no goals
case intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
this : ¬Set.Countable (E ∩ D)
h : ∀ (x_1 : α), x_1 ∈ E ∩ (C \ V) → x_1 = x
⊢ False
exact absurd (Countable.mono h (Set.countable_singleton _)) this
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : Set.Countable (E ∩ D)
⊢ False
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
⊢ ¬Set.Countable (E ∩ D)
intro h
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : Set.Countable (E ∩ D)
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
⊢ False
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : Set.Countable (E ∩ D)
⊢ False
obtain ⟨U, hUb, xU, hU⟩ : ∃ U ∈ b, x ∈ U ∧ U ⊆ E :=
  (IsTopologicalBasis.mem_nhds_iff bbasis).mp xE
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : Set.Countable (E ∩ D)
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
hU_cnt : Set.Countable (U ∩ C)
this : U ∈ v
⊢ False
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : Set.Countable (E ∩ D)
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
hU_cnt : Set.Countable (U ∩ C)
⊢ False
have : U ∈ v := ⟨hUb, hU_cnt⟩
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : Set.Countable (E ∩ D)
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
hU_cnt : Set.Countable (U ∩ C)
this : U ∈ v
⊢ x ∈ V
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : Set.Countable (E ∩ D)
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
hU_cnt : Set.Countable (U ∩ C)
this : U ∈ v
⊢ False
apply xD.2
no goals
case intro.intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : Set.Countable (E ∩ D)
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
hU_cnt : Set.Countable (U ∩ C)
this : U ∈ v
⊢ x ∈ V
exact mem_biUnion this xU
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : Set.Countable (E ∩ D)
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
⊢ U ∩ C ⊆ E ∩ D ∪ V ∩ C

case a
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : Set.Countable (E ∩ D)
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
⊢ Set.Countable (E ∩ D ∪ V ∩ C)
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : Set.Countable (E ∩ D)
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
⊢ Set.Countable (U ∩ C)
apply @Countable.mono _ _ (E ∩ D ∪ V ∩ C)
no goals
case a
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : Set.Countable (E ∩ D)
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
⊢ Set.Countable (E ∩ D ∪ V ∩ C)
exact Countable.union h Vct
case h.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : Set.Countable (E ∩ D)
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
y : α
yU : y ∈ U
yC : y ∈ C
⊢ y ∈ E ∩ D ∪ V ∩ C
case h
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : Set.Countable (E ∩ D)
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
⊢ U ∩ C ⊆ E ∩ D ∪ V ∩ C
rintro y ⟨yU, yC⟩
case pos
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h✝ : Set.Countable (E ∩ D)
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
y : α
yU : y ∈ U
yC : y ∈ C
h : y ∈ V
⊢ y ∈ E ∩ D ∪ V ∩ C

case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h✝ : Set.Countable (E ∩ D)
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
y : α
yU : y ∈ U
yC : y ∈ C
h : ¬y ∈ V
⊢ y ∈ E ∩ D ∪ V ∩ C
case h.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h : Set.Countable (E ∩ D)
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
y : α
yU : y ∈ U
yC : y ∈ C
⊢ y ∈ E ∩ D ∪ V ∩ C
by_cases h : y ∈ V
no goals
case pos
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h✝ : Set.Countable (E ∩ D)
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
y : α
yU : y ∈ U
yC : y ∈ C
h : y ∈ V
⊢ y ∈ E ∩ D ∪ V ∩ C
exact mem_union_right _ (mem_inter h yC)
no goals
case neg
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
x : α
xD : x ∈ D
E : Set α
xE : E ∈ 𝓝 x
h✝ : Set.Countable (E ∩ D)
U : Set α
hUb : U ∈ b
xU : x ∈ U
hU : U ⊆ E
y : α
yU : y ∈ U
yC : y ∈ C
h : ¬y ∈ V
⊢ y ∈ E ∩ D ∪ V ∩ C
exact mem_union_left _ (mem_inter (hU yU) ⟨yC, h⟩)
no goals
case intro.intro.intro.refine'_3
α : Type u_1
inst✝¹ : TopologicalSpace α
C : Set α
inst✝ : SecondCountableTopology α
hclosed : IsClosed C
b : Set (Set α)
bct : Set.Countable b
left✝ : ¬∅ ∈ b
bbasis : IsTopologicalBasis b
v : Set (Set α) := {U | U ∈ b ∧ Set.Countable (U ∩ C)}
V : Set α := ⋃ (U : Set α) (_ : U ∈ v), U
D : Set α := C \ V
Vct : Set.Countable (V ∩ C)
⊢ C = V ∩ C ∪ D
rw [inter_comm, inter_union_diff]