Theorem Ico_mem_nhds_iff

Modification history

2024-04-08 07:22
Mathlib/Topology/Order/Basic.lean
refactor(Topology/Order/Basic): split up large file (#11992) …
Modified Ico_mem_nhds_iffView on Github →
2024-03-12 01:07
Mathlib/Topology/Order/Basic.lean
feat: `@[simp]` `Icc a b ∈ 𝓝 x` (#11178) …
Added Ico_mem_nhds_iffView on Github →