dist_lt_iff — Mathlib

English

If 0 < C, then dist f g < C if and only if ∀ x, dist(f(x), g(x)) < C.

Русский

Если 0 < C, то dist f g < C тогда и только тогда, когда ∀ x, dist(f(x), g(x)) < C.

LaTeX

$$$\text{dist\_lt\_iff} (C>0) : dist f g < C \iff \forall x, dist(f(x), g(x)) < C$$$

Lean4

theorem dist_lt_iff (C0 : (0 : ℝ) < C) : dist f g < C ↔ ∀ x : α, dist (f x) (g x) < C :=
  by
  rw [← dist_mkOfCompact, dist_lt_iff_of_compact C0]
  simp only [mkOfCompact_apply]

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