Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-01-07 20:33
06c19488
View on Github →
chore: protect
Filter.nhds_{iInf,inf}
(
#20530
) Per
Zulip
Estimated changes
Modified
Mathlib/Topology/Filter.lean
deleted
theorem
Filter.nhds_iInf
deleted
theorem
Filter.nhds_inf