lipschitzOnWith_empty — Mathlib

English

Any function is Lipschitz on the empty set with any Lipschitz constant.

Русский

Любая функция Lipschitz на пустом множестве с произвольной константой Липшица.

LaTeX

$$LipschitzOnWith(K, f, \emptyset)$$

Lean4

/-- Every function is Lipschitz on the empty set (with any Lipschitz constant). -/
@[simp]
theorem lipschitzOnWith_empty (K : ℝ≥0) (f : α → β) : LipschitzOnWith K f ∅ := fun _ => False.elim

Похожие утверждения