dist_le_iff_of_nonempty — Mathlib

English

If α is nonempty, then dist f g ≤ C iff ∀ x, dist(f x) (g x) ≤ C.

Русский

Если область определения непустая, то dist(f,g) ≤ C эквивалентно ∀ x, dist(f(x), g(x)) ≤ C.

LaTeX

$$$[Nonempty \alpha] : \operatorname{dist}(f,g) \le C \iff \forall x:\alpha, \operatorname{dist}(f(x), g(x)) \le C$$$

Lean4

theorem dist_le_iff_of_nonempty [Nonempty α] : dist f g ≤ C ↔ ∀ x, dist (f x) (g x) ≤ C :=
  ⟨fun h x => le_trans (dist_coe_le_dist x) h, fun w => (dist_le (le_trans dist_nonneg (w (Nonempty.some ‹_›)))).mpr w⟩

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