dist_lt_iff_of_compact — Mathlib

English

If α is nonempty and compact, 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] [CompactSpace \alpha] : dist f g < C \iff \forall x:\alpha, dist(f(x), g(x)) < C$$$

Lean4

theorem dist_lt_iff_of_compact [CompactSpace α] (C0 : (0 : ℝ) < C) : dist f g < C ↔ ∀ x : α, dist (f x) (g x) < C :=
  by
  fconstructor
  · intro w x
    exact lt_of_le_of_lt (dist_coe_le_dist x) w
  · by_cases h : Nonempty α
    · exact dist_lt_of_nonempty_compact
    · rintro -
      convert C0
      apply le_antisymm _ dist_nonneg'
      rw [dist_eq]
      exact csInf_le ⟨0, fun C => And.left⟩ ⟨le_rfl, fun x => False.elim (h (Nonempty.intro x))⟩

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