Theorem isOpen_Iio'

Modification history

2026-04-21 17:27
Mathlib/Topology/Order/Basic.lean
chore(Topology/Order/Basic): use `to_dual` (#37780)
Deleted isOpen_Iio'View on Github →
2025-09-11 07:52
Mathlib/Topology/Order/Basic.lean
feat: the topology on WithTop is second countable (#29466)
Added isOpen_Iio'View on Github →