boundedSub_of_lipschitzWith_sub — Mathlib

English

If there exists a Lipschitz bound for the subtraction map on R×R, then bounded subtraction is possible: for bounded s,t, s − t is bounded.

Русский

Если существует предел Липшица для минус-операции на R×R, то разность множеств s−t ограничена при ограниченных s,t.

LaTeX

$$$\forall s,t\subseteq R,\ IsBounded(s) \land IsBounded(t) \Rightarrow IsBounded(s \setminus t)$$$

Lean4

theorem boundedSub_of_lipschitzWith_sub [PseudoMetricSpace R] [Sub R] {K : NNReal}
    (lip : LipschitzWith K (fun (p : R × R) ↦ p.1 - p.2)) : BoundedSub R where
  isBounded_sub {s t} s_bdd
    t_bdd := by
    have bdd : Bornology.IsBounded (s ×ˢ t) := Bornology.IsBounded.prod s_bdd t_bdd
    convert lip.isBounded_image bdd
    simp

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