Theorem Ordinal.nhdsLT_eq_nhdsNE

Modification history

2025-02-17 19:20

Mathlib/SetTheory/Ordinal/Topology.lean

chore(SetTheory/Ordinal/Topology): generalize theorems to `SuccOrder` (#20491) …

Modified Ordinal.nhdsLT_eq_nhdsNE View on Github →

2024-12-23 08:37

Mathlib/SetTheory/Ordinal/Topology.lean

chore(*): rename lemmas about `𝓝[≥] a` etc (#20188) …

Added Ordinal.nhdsLT_eq_nhdsNE View on Github →