isUniformInducing_pi_restrict — Mathlib

English

The map sending f to its family of restricted coordinates is uniform inducing with respect to the π-structure.

Русский

Отображение, отправляющее f в семейство ограниченных координат, равно по отношению к π-структуре равномерно индуцирующее.

LaTeX

$$IsUniformInducing (fun f => fun s => UniformFun.ofFun ((s : Set α).restrict (toFun 𝔖 f))).$$

Lean4

/-- The map sending a function `f : α →ᵤ[𝔖] β` to the family of restrictions of `f` to each `s ∈ 𝔖`
(each coordinate equipped with its respective uniform structure `s →ᵤ β`) induces the uniformity on
`α →ᵤ[𝔖] β`. -/
theorem isUniformInducing_pi_restrict :
    IsUniformInducing (fun f : α →ᵤ[𝔖] β ↦ fun s : 𝔖 ↦ UniformFun.ofFun ((s : Set α).restrict (toFun 𝔖 f))) :=
  by
  simp_rw [isUniformInducing_iff_uniformSpace, Pi.uniformSpace_eq, UniformSpace.comap_iInf, ← UniformSpace.comap_comap,
    iInf_subtype]
  rfl

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