isClosed_setOf_lipschitzWith — Mathlib

English

The set of LipschitzWith functions is closed in the universal domain, i.e., LipschitzWith on all of α.

Русский

Множество LipschitzWith на всей области α замкнуто.

LaTeX

$$$\text{IsClosed }\{f: \alpha \to \beta \mid \text{LipschitzWith } K\ f\}$.$$

Lean4

theorem isClosed_setOf_lipschitzWith {α β} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : ℝ≥0) :
    IsClosed {f : α → β | LipschitzWith K f} := by simp only [← lipschitzOnWith_univ, isClosed_setOf_lipschitzOnWith]

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