Skip to content

Commit aa204e9

Browse files
committed
Update docstring of squeeze_one_norm' (#8667)
`squeeze_one_norm'` and `squeeze_zero_norm'` had the same docstring. The docstring of `squeeze_zero_norm'` was strictly speaking incorrect (writing `1` instead of `0`). The docstring of `squeeze_one_norm'` was correct but perhaps this change makes it easier for people to notice the difference and what `E` is.
1 parent 7cc262f commit aa204e9

File tree

1 file changed

+5
-5
lines changed

1 file changed

+5
-5
lines changed

Mathlib/Analysis/Normed/Group/Basic.lean

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1096,12 +1096,12 @@ theorem comap_norm_nhds_one : comap norm (𝓝 0) = 𝓝 (1 : E) := by
10961096
#align comap_norm_nhds_zero comap_norm_nhds_zero
10971097

10981098
/-- Special case of the sandwich theorem: if the norm of `f` is eventually bounded by a real
1099-
function `a` which tends to `0`, then `f` tends to `1`. In this pair of lemmas (`squeeze_one_norm'`
1100-
and `squeeze_one_norm`), following a convention of similar lemmas in `Topology.MetricSpace.Basic`
1101-
and `Topology.Algebra.Order`, the `'` version is phrased using "eventually" and the non-`'` version
1102-
is phrased absolutely. -/
1099+
function `a` which tends to `0`, then `f` tends to `1` (neutral element of `SeminormedGroup`).
1100+
In this pair of lemmas (`squeeze_one_norm'` and `squeeze_one_norm`), following a convention of
1101+
similar lemmas in `Topology.MetricSpace.Basic` and `Topology.Algebra.Order`, the `'` version is
1102+
phrased using "eventually" and the non-`'` version is phrased absolutely. -/
11031103
@[to_additive "Special case of the sandwich theorem: if the norm of `f` is eventually bounded by a
1104-
real function `a` which tends to `0`, then `f` tends to `1`. In this pair of lemmas
1104+
real function `a` which tends to `0`, then `f` tends to `0`. In this pair of lemmas
11051105
(`squeeze_zero_norm'` and `squeeze_zero_norm`), following a convention of similar lemmas in
11061106
`Topology.MetricSpace.PseudoMetric` and `Topology.Algebra.Order`, the `'` version is phrased using
11071107
\"eventually\" and the non-`'` version is phrased absolutely."]

0 commit comments

Comments
 (0)