dist_set_exists — Mathlib

English

There exists a nonnegative C such that for all x, dist(f(x), g(x)) ≤ C.

Русский

Существует неотрицательное C такое, что для всех x выполняется dist(f(x), g(x)) ≤ C.

LaTeX

$$$\exists C\, 0 \le C \wedge \forall x:\alpha, \operatorname{dist}(f(x), g(x)) \le C$$$

Lean4

theorem dist_set_exists : ∃ C, 0 ≤ C ∧ ∀ x : α, dist (f x) (g x) ≤ C :=
  by
  rcases isBounded_iff.1 (f.isBounded_range.union g.isBounded_range) with ⟨C, hC⟩
  refine ⟨max 0 C, le_max_left _ _, fun x => (hC ?_ ?_).trans (le_max_right _ _)⟩ <;> [left; right] <;>
    apply mem_range_self

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