dist_lt_of_nonempty_compact — Mathlib

English

If α is nonempty and compact and dist(f x, g x) < C for all x, then dist(f,g) < C.

Русский

Если область определения непустая и компактна и для всех x выполняется dist(fx, gx) < C, то dist(f,g) < C.

LaTeX

$$$[Nonempty \alpha] [CompactSpace \alpha] (w : \forall x:\alpha, \operatorname{dist}(f(x), g(x)) < C) : \operatorname{dist}(f,g) < C$$$

Lean4

theorem dist_lt_of_nonempty_compact [Nonempty α] [CompactSpace α] (w : ∀ x : α, dist (f x) (g x) < C) : dist f g < C :=
  by
  have c : Continuous fun x => dist (f x) (g x) := by fun_prop
  obtain ⟨x, -, le⟩ := IsCompact.exists_isMaxOn isCompact_univ Set.univ_nonempty (Continuous.continuousOn c)
  exact lt_of_le_of_lt (dist_le_iff_of_nonempty.mpr fun y => le trivial) (w x)

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