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