Theorem nhdsGT_basis_Ioc_of_exists_gt

Modification history

2026-06-20 03:53
Mathlib/Topology/Order/LeftRightNhds.lean
feat: in a dense order, `𝓝[<] a` has `fun x ↦ Ico x a` as a basis (#40523)
Added nhdsGT_basis_Ioc_of_exists_gtView on Github →