Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-01-23 13:42
2a76c1de
View on Github →
feat(Topology/Order): add
nhdsWithin_Ici_basis_Icc
(
#9913
)
Estimated changes
Modified
Mathlib/Topology/Order/Basic.lean
added
theorem
nhdsWithin_Ici_basis_Icc
added
theorem
nhdsWithin_Iic_basis_Icc