Theorem Ioc_mem_nhds_iff

Modification history

2026-10-05 09:13
Mathlib/Topology/Order/DenselyOrdered.lean
feat: tag `Function.leftLim` with `to_dual` (#43525)
Deleted Ioc_mem_nhds_iffView on Github →
2024-04-08 07:22
Mathlib/Topology/Order/Basic.lean
refactor(Topology/Order/Basic): split up large file (#11992) …
Modified Ioc_mem_nhds_iffView on Github →
2024-03-12 01:07
Mathlib/Topology/Order/Basic.lean
feat: `@[simp]` `Icc a b ∈ 𝓝 x` (#11178) …
Added Ioc_mem_nhds_iffView on Github →