case h.e'_2.h.e'_2.h.e'_2.h.h.a
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
e_1✝ : α = (fun x => αᵒᵈ) a
x✝ : α
⊢ x✝ ⋖ a ↔ ↑toDual a ⋖ x✝
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
⊢ 𝓝[Iio a] a = ⊥ ↔ IsBot a ∨ ∃ b, b ⋖ a
convert (config := {preTransparency := .default})
  nhdsWithin_Ioi_eq_bot_iff (a := OrderDual.toDual a) using 4
no goals
case h.e'_2.h.e'_2.h.e'_2.h.h.a
α : Type u
β : Type v
γ : Type w
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
e_1✝ : α = (fun x => αᵒᵈ) a
x✝ : α
⊢ x✝ ⋖ a ↔ ↑toDual a ⋖ x✝
exact ofDual_covby_ofDual_iff