Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-11-08 15:06
31c320e6
View on Github →
feat: define
Filter.IsApproximateUnit
and basic API (
#17787
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/Topology/ApproximateUnit.lean
added
theorem
Filter.IsApproximateUnit.iff_le_nhds_one
added
theorem
Filter.IsApproximateUnit.iff_neBot_and_le_nhds_one
added
theorem
Filter.IsApproximateUnit.mono
added
theorem
Filter.IsApproximateUnit.nhds_one
added
theorem
Filter.IsApproximateUnit.pure_one
added
structure
Filter.IsApproximateUnit