Theorem CovBy.nhdsWithin_Ioi

Modification history

2024-11-11 05:16

Mathlib/Topology/Order/OrderClosed.lean

feat(Topology/Order): add more `CovBy.nhdsWithin...` lemmas (#18567) …

Deleted CovBy.nhdsWithin_Ioi View on Github →

2024-02-13 23:17

Mathlib/Topology/Order/Basic.lean

chore(Topology/Order): move `OrderClosedTopology` to a new file (#10497)

Modified CovBy.nhdsWithin_Ioi View on Github →

2024-01-09 09:25

Mathlib/Topology/Order/Basic.lean

chore(Covby): rename `Covby` to `CovBy` (#9578) …

Added CovBy.nhdsWithin_Ioi View on Github →