English
If f and g are bounded functions X → R, then their difference f − g is bounded.
Русский
Если f и g ограничены функции X → R, то их разность f − g ограничена.
LaTeX
$$$\forall X\;\forall f,g: X\to R,\big(\exists C,\forall x,y,|f(x)-f(y)|\le C\big) \land \big(\exists C,\forall x,y,|g(x)-g(y)|\le C\big) \Rightarrow \exists C,\forall x,y,| (f-g)(x)-(f-g)(y)| \le C$$$
Lean4
theorem sub_bounded_of_bounded_of_bounded {X : Type*} [PseudoMetricSpace R] [Sub R] [BoundedSub R] {f g : X → R}
(f_bdd : ∃ C, ∀ x y, dist (f x) (f y) ≤ C) (g_bdd : ∃ C, ∀ x y, dist (g x) (g y) ≤ C) :
∃ C, ∀ x y, dist ((f - g) x) ((f - g) y) ≤ C :=
by
obtain ⟨C, hC⟩ :=
Metric.isBounded_iff.mp <|
isBounded_sub (Metric.isBounded_range_iff.mpr f_bdd) (Metric.isBounded_range_iff.mpr g_bdd)
use C
intro x y
exact
hC (Set.sub_mem_sub (Set.mem_range_self (f := f) x) (Set.mem_range_self (f := g) x))
(Set.sub_mem_sub (Set.mem_range_self (f := f) y) (Set.mem_range_self (f := g) y))
