uniformContinuous_coe — Mathlib

English

The map f ↦ f (as a function) is uniformly continuous from α →ᵇ β to α → β.

Русский

Отображение f ↦ f (как функция) из α →ᵇ β в α → β одинаково непрерывно по униформной структуре.

LaTeX

$$uniformContinuous_coe$$

Lean4

theorem uniformContinuous_coe : @UniformContinuous (α →ᵇ β) (α → β) _ _ (⇑) :=
  uniformContinuous_pi.2 fun x => (lipschitz_evalx x).uniformContinuous

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