Theorem frequently_gt_nhds

Modification history

2026-03-05 12:46

Mathlib/Topology/Order/LeftRight.lean

chore(Topology/Order/LeftRight): use `to_dual` (#35637) …

Deleted frequently_gt_nhds View on Github →

2023-10-30 03:09

Mathlib/Topology/Algebra/Order/LeftRight.lean

feat: `∃ᶠ x in 𝓝 a, x < a` (#7941) …

Added frequently_gt_nhds View on Github →