English
If f,g: X → R are bounded, then their pointwise product f·g is bounded.
Русский
Если функции f,g: X → R ограничены, то их точечное произведение f·g ограничено.
LaTeX
$$$\forall x,y,\; IsBounded((f\cdot g)(x))-(f\cdot g)(y)\le C$$$
Lean4
@[to_additive]
theorem mul_bounded_of_bounded_of_bounded {X : Type*} [PseudoMetricSpace R] [Mul R] [BoundedMul 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_mul (Metric.isBounded_range_iff.mpr f_bdd) (Metric.isBounded_range_iff.mpr g_bdd)
use C
intro x y
exact
hC (Set.mul_mem_mul (Set.mem_range_self (f := f) x) (Set.mem_range_self (f := g) x))
(Set.mul_mem_mul (Set.mem_range_self (f := f) y) (Set.mem_range_self (f := g) y))
