Theorem NNReal.lipschitzWith_sub

Modification history

2024-09-05 04:39
Mathlib/Analysis/Normed/Field/Basic.lean
chore: split Analysis.Normed.Field.Basic (#16479)
Modified NNReal.lipschitzWith_subView on Github →
2024-05-22 15:10
Mathlib/Analysis/Normed/Field/Basic.lean
feat: BoundedAdd class for consistency with BoundedSub and BoundedMul. (#13035) …
Added NNReal.lipschitzWith_subView on Github →