You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: templates/extras/pitfalls.md
+1-1Lines changed: 1 addition & 1 deletion
Display the source diff
Display the rich diff
Original file line number
Diff line number
Diff line change
@@ -401,7 +401,7 @@ Consider adding `Summable f` hypotheses to theorems that involve `∑' i, f i`.
401
401
-`Nat.sqrt x` takes the floor of $\sqrt{x}$.
402
402
-`Real.sqrt x` is `0` for negative inputs.
403
403
-`Real.log x` actually means $\log_e |x|$ when $x \ne 0$ and is $0$ when $x = 0$.
404
-
This gives nicer algebraic properties then setting it to be $0$ for negative all $x$.
404
+
This gives nicer algebraic properties than setting it to be $0$ for all negative $x$.
405
405
-`Real.sSup` and `Real.iSup` are 0 if the set is empty or not bounded above, and likewise `Real.sInf`, and `Real.iInf` are 0 if the set is empty or not bounded below.
406
406
This interacts nicely with `Real.sqrt`: it means that $\sqrt{x} = \sup \{y \mid y^2 < x\}$ for all $x \in \mathbb{R}$, since when $x \le 0$ both sides are $0$.
0 commit comments