isClosed_setOf_lipschitzOnWith — Mathlib

English

For LipschitzWith function family, the set of such functions is closed when restricted to a set S.

Русский

Множество функций LipschitzOnWith на области S замкнуто.

LaTeX

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

Lean4

theorem isClosed_setOf_lipschitzOnWith {α β} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : ℝ≥0) (s : Set α) :
    IsClosed {f : α → β | LipschitzOnWith K f s} :=
  by
  simp only [LipschitzOnWith, setOf_forall]
  refine isClosed_biInter fun x _ => isClosed_biInter fun y _ => isClosed_le ?_ ?_
  exacts [.edist (continuous_apply x) (continuous_apply y), continuous_const]

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