Commit 2024-02-14 01:35 c9ad2c58

View on Github →

refactor(WithZeroTopology): use nhdsAdjoint (#10411) It's more specialized than mkOfNhds. Also golf and rename lemmas about nhdsAdjoint.

Estimated changes

Modified Mathlib/Topology/Algebra/WithZeroTopology.lean

modified theorem WithZeroTopology.nhds_eq_update

modified theorem WithZeroTopology.nhds_of_ne_zero

modified theorem WithZeroTopology.nhds_zero

Modified Mathlib/Topology/Order.lean

modified theorem le_nhdsAdjoint_iff'

deleted theorem nhdsAdjoint_nhds

modified theorem nhdsAdjoint_nhds_of_ne

added theorem nhds_nhdsAdjoint

added theorem nhds_nhdsAdjoint_of_ne

added theorem nhds_nhdsAdjoint_same