comap_eq — Mathlib

English

If f is uniformly continuous, then postcomposition by f is uniformly continuous on α →ᵤ β.

Русский

Если f равномерно непрерывен, то пост-композиция f ∘ · — равномерно непрерывна на α →ᵤ β.

LaTeX

$$$$ \text{If } f: γ \to β \text{ is uniformly continuous, then } (f \circ \cdot): (α \to^{u} γ) \to (α \to^{u} β) \text{ is uniformly continuous}. $$$$

Lean4

/-- If `u` is a uniform structures on `β` and `f : γ → β`, then
`𝒰(α, γ, comap f u) = comap (fun g ↦ f ∘ g) 𝒰(α, γ, u₁)`. -/
protected theorem comap_eq {f : γ → β} : 𝒰(α, γ, ‹UniformSpace β›.comap f) = 𝒰(α, β, _).comap (f ∘ ·) :=
  by
  letI : UniformSpace γ := .comap f ‹_›
  exact (UniformFun.postcomp_isUniformInducing (f := f) ⟨rfl⟩).comap_uniformSpace.symm

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