uniformContinuous_of_const — Mathlib

English

If a function c is constant (c a = c b for all a,b), then c is uniformly continuous.

Русский

Если функция константна, то она является равномерно непрерывной.

LaTeX

$$$ (\forall a,b,\; c(a)=c(b)) \;\Rightarrow\; UniformContinuous\, c. $$$

Lean4

theorem uniformContinuous_of_const [UniformSpace β] {c : α → β} (h : ∀ a b, c a = c b) : UniformContinuous c :=
  have : (fun x : α × α => (c x.fst, c x.snd)) ⁻¹' idRel = univ := eq_univ_iff_forall.2 fun ⟨a, b⟩ => h a b
  le_trans (map_le_iff_le_comap.2 <| by simp [comap_principal, this]) refl_le_uniformity

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