case pos
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : IsTop a
⊢ 𝓝[Ioi a] a = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b

case neg
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : ¬IsTop a
⊢ 𝓝[Ioi a] a = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
⊢ 𝓝[Ioi a] a = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b
by_cases ha : IsTop a
no goals
case pos
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : IsTop a
⊢ 𝓝[Ioi a] a = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b
simp [ha, ha.isMax.Ioi_eq]
case neg
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : ¬IsTop a
⊢ 𝓝[Ioi a] a = ⊥ ↔ ∃ b, a ⋖ b
case neg
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : ¬IsTop a
⊢ 𝓝[Ioi a] a = ⊥ ↔ IsTop a ∨ ∃ b, a ⋖ b
simp only [ha, false_or]
case neg
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : ∃ b, a < b
⊢ 𝓝[Ioi a] a = ⊥ ↔ ∃ b, a ⋖ b
case neg
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : ¬IsTop a
⊢ 𝓝[Ioi a] a = ⊥ ↔ ∃ b, a ⋖ b
rw [isTop_iff_isMax, not_isMax_iff] at ha
no goals
case neg
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
ha : ∃ b, a < b
⊢ 𝓝[Ioi a] a = ⊥ ↔ ∃ b, a ⋖ b
simp only [(nhdsWithin_Ioi_basis' ha).eq_bot_iff, covby_iff_Ioo_eq]