case h
α : Type u
⊢ ∀ (x : α), IsOpen {x}
α : Type u
⊢ induced pure Ultrafilter.topologicalSpace = ⊥
apply eq_bot_of_singletons_open
case h
α : Type u
x : α
⊢ IsOpen {x}
case h
α : Type u
⊢ ∀ (x : α), IsOpen {x}
intro x
case h
α : Type u
x : α
⊢ pure ⁻¹' {u | {x} ∈ u} = {x}
case h
α : Type u
x : α
⊢ IsOpen {x}
use { u : Ultrafilter α | {x} ∈ u }, ultrafilter_isOpen_basic _
no goals
case h
α : Type u
x : α
⊢ pure ⁻¹' {u | {x} ∈ u} = {x}
simp