case intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
x y : α
hy : x < y
⊢ Disjoint (𝓝 x) atTop
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
x : α
⊢ Disjoint (𝓝 x) atTop
rcases exists_gt x with ⟨y, hy : x < y⟩
case intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
x y : α
hy : x < y
⊢ Disjoint (Iio y) {b | y ≤ b}
case intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
x y : α
hy : x < y
⊢ Disjoint (𝓝 x) atTop
refine' disjoint_of_disjoint_of_mem _ (Iio_mem_nhds hy) (mem_atTop y)
no goals
case intro
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
x y : α
hy : x < y
⊢ Disjoint (Iio y) {b | y ≤ b}
exact disjoint_left.mpr fun z => not_le.2