case h.e'_2.h.h.e'_2.h.h.h.e'_2.h.h.a
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
e_1✝² e_1✝¹ : α = αᵒᵈ
x✝¹ : α
e_1✝ : α = αᵒᵈ
x✝ : α
⊢ x✝ ⋖ x✝¹ ↔ x✝¹ ⋖ x✝
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
⊢ Set.Countable {x | ∃ y, y ⋖ x}
convert @countable_setOf_covby_right αᵒᵈ _ _ _ _ using 5
no goals
case h.e'_2.h.h.e'_2.h.h.h.e'_2.h.h.a
α : Type u
β : Type v
γ : Type w
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : SecondCountableTopology α
e_1✝² e_1✝¹ : α = αᵒᵈ
x✝¹ : α
e_1✝ : α = αᵒᵈ
x✝ : α
⊢ x✝ ⋖ x✝¹ ↔ x✝¹ ⋖ x✝
exact toDual_covby_toDual_iff.symm