uniformContinuous_toFun — Mathlib

English

There is a natural uniform isomorphism between α →ᵤ β × γ and (α →ᵤ β) × (α →ᵤ γ).

Русский

Существует естественный равномерный изоморфизм между α →ᵤ β × γ и (α →ᵤ β) × (α →ᵤ γ).

LaTeX

$$$$ (α →^{u} β \times γ) \simeq_{u} (α →^{u} β) \times (α →^{u} γ). $$$$

Lean4

/-- The natural map `UniformFun.toFun` from `α →ᵤ β` to `α → β` is uniformly continuous.

In other words, the uniform structure of uniform convergence is finer than that of pointwise
convergence, aka the product uniform structure. -/
protected theorem uniformContinuous_toFun : UniformContinuous (toFun : (α →ᵤ β) → α → β) := by
  -- By definition of the product uniform structure, this is just `uniform_continuous_eval`.

  rw [uniformContinuous_pi]
  intro x
  exact uniformContinuous_eval β x

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