Theorem Filter.IsApproximateUnit.nhds_one

Modification history

2026-03-13 18:00

Mathlib/Topology/ApproximateUnit.lean

feat: generalize some `ContinuousMul` hypotheses to `SeparatelyContinuousMul` (#36562) …

Modified Filter.IsApproximateUnit.nhds_one View on Github →

2024-11-08 15:06

Mathlib/Topology/ApproximateUnit.lean

feat: define `Filter.IsApproximateUnit` and basic API (#17787)

Added Filter.IsApproximateUnit.nhds_one View on Github →