Theorem NNReal.lipschitzWith_sub

Modification history

2025-03-09 23:03
Mathlib/Analysis/Normed/Field/Lemmas.lean
refactor(Mathlib/Analysis/Normed): disentangle normed rings and normed fields (#22744) …
Modified NNReal.lipschitzWith_subView on Github →
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 →