α : Type u_1
β : Type ?u.26837
γ : Type ?u.26840
γ₂ : Type ?u.26843
δ : Type ?u.26846
ι : Sort y
s✝ t u : Set α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : Countable α
s : Set α
x✝ : MeasurableSet s
⊢ MeasurableSet (⋃ (x : α) (_ : x ∈ s), {x})
α : Type u_1
β : Type ?u.26837
γ : Type ?u.26840
γ₂ : Type ?u.26843
δ : Type ?u.26846
ι : Sort y
s t u : Set α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : Countable α
⊢ borel α = ⊤
refine' top_le_iff.1 fun s _ => biUnion_of_singleton s ▸ _
α : Type u_1
β : Type ?u.26837
γ : Type ?u.26840
γ₂ : Type ?u.26843
δ : Type ?u.26846
ι : Sort y
s✝ t u : Set α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : Countable α
s : Set α
x✝ : MeasurableSet s
⊢ ∀ (b : α), b ∈ s → MeasurableSet {b}
α : Type u_1
β : Type ?u.26837
γ : Type ?u.26840
γ₂ : Type ?u.26843
δ : Type ?u.26846
ι : Sort y
s✝ t u : Set α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : Countable α
s : Set α
x✝ : MeasurableSet s
⊢ MeasurableSet (⋃ (x : α) (_ : x ∈ s), {x})
apply MeasurableSet.biUnion s.to_countable
α : Type u_1
β : Type ?u.26837
γ : Type ?u.26840
γ₂ : Type ?u.26843
δ : Type ?u.26846
ι : Sort y
s✝ t u : Set α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : Countable α
s : Set α
x✝ : MeasurableSet s
x : α
a✝ : x ∈ s
⊢ MeasurableSet {x}
α : Type u_1
β : Type ?u.26837
γ : Type ?u.26840
γ₂ : Type ?u.26843
δ : Type ?u.26846
ι : Sort y
s✝ t u : Set α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : Countable α
s : Set α
x✝ : MeasurableSet s
⊢ ∀ (b : α), b ∈ s → MeasurableSet {b}
intro x _
case h
α : Type u_1
β : Type ?u.26837
γ : Type ?u.26840
γ₂ : Type ?u.26843
δ : Type ?u.26846
ι : Sort y
s✝ t u : Set α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : Countable α
s : Set α
x✝ : MeasurableSet s
x : α
a✝ : x ∈ s
⊢ MeasurableSet ({x}ᶜ)
α : Type u_1
β : Type ?u.26837
γ : Type ?u.26840
γ₂ : Type ?u.26843
δ : Type ?u.26846
ι : Sort y
s✝ t u : Set α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : Countable α
s : Set α
x✝ : MeasurableSet s
x : α
a✝ : x ∈ s
⊢ MeasurableSet {x}
apply MeasurableSet.of_compl
case h.a
α : Type u_1
β : Type ?u.26837
γ : Type ?u.26840
γ₂ : Type ?u.26843
δ : Type ?u.26846
ι : Sort y
s✝ t u : Set α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : Countable α
s : Set α
x✝ : MeasurableSet s
x : α
a✝ : x ∈ s
⊢ {x}ᶜ ∈ {s | IsOpen s}
case h
α : Type u_1
β : Type ?u.26837
γ : Type ?u.26840
γ₂ : Type ?u.26843
δ : Type ?u.26846
ι : Sort y
s✝ t u : Set α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : Countable α
s : Set α
x✝ : MeasurableSet s
x : α
a✝ : x ∈ s
⊢ MeasurableSet ({x}ᶜ)
apply GenerateMeasurable.basic
no goals
case h.a
α : Type u_1
β : Type ?u.26837
γ : Type ?u.26840
γ₂ : Type ?u.26843
δ : Type ?u.26846
ι : Sort y
s✝ t u : Set α
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : Countable α
s : Set α
x✝ : MeasurableSet s
x : α
a✝ : x ∈ s
⊢ {x}ᶜ ∈ {s | IsOpen s}
exact isClosed_singleton.isOpen_compl