α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTop α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
this : ∃ x, x < ⊤
⊢ HasBasis (𝓝 ⊤) (fun a => a < ⊤) fun a => Ioi a
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTop α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
⊢ HasBasis (𝓝 ⊤) (fun a => a < ⊤) fun a => Ioi a
have : ∃ x : α, x < ⊤ := (exists_ne ⊤).imp fun x hx => hx.lt_top
no goals
α : Type u
β : Type v
γ : Type w
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTop α
inst✝¹ : OrderTopology α
inst✝ : Nontrivial α
this : ∃ x, x < ⊤
⊢ HasBasis (𝓝 ⊤) (fun a => a < ⊤) fun a => Ioi a
simpa only [Iic_top, nhdsWithin_univ, Ioc_top] using nhdsWithin_Iic_basis' this