dist_lt_iff_of_nonempty_compact — Mathlib

English

For [CompactSpace α], and C0 > 0, dist f g < C iff ∀ x, dist(f x) (g x) < C.

Русский

Для компактного пространства α и C>0, dist(f,g) < C эквивалентно ∀ x, dist(f(x), g(x)) < C.

LaTeX

$$$[CompactSpace \alpha] (C0 : 0 < C) : dist f g < C \iff \forall x:\alpha, dist(f(x), g(x)) < C$$$

Lean4

theorem dist_lt_iff_of_nonempty_compact [Nonempty α] [CompactSpace α] : dist f g < C ↔ ∀ x : α, dist (f x) (g x) < C :=
  ⟨fun w x => lt_of_le_of_lt (dist_coe_le_dist x) w, dist_lt_of_nonempty_compact⟩

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