Theorem LipschitzWith.div

Modification history

2024-08-26 10:46

Mathlib/Analysis/Normed/Group/Uniform.lean

feat: Local lipschitzness under pointwise operations (#16115)

Modified LipschitzWith.div View on Github →

2024-06-20 19:07

Mathlib/Analysis/Normed/Group/Basic.lean

chore: move some lemmas to Analysis.Normed.Group.Uniform (#13945) …

Modified LipschitzWith.div View on Github →

2023-03-09 06:58

Mathlib/Analysis/Normed/Group/Basic.lean

feat: port Analysis.Normed.Group.Basic (#2736)

Added LipschitzWith.div View on Github →