isUniformInducing_coeFn — Mathlib

English

The coercion map from UniformConvergenceCLM to UniformOnFun is a uniform inducing map.

Русский

Отображение приведения к UniformOnFun непрерывно индуцирует uniform пространство.

LaTeX

$$$\\operatorname{IsUniformInducing}\\left(\\alpha := \\mathrm{UniformConvergenceCLM}(\\sigma, F, 𝔖),\\; \\mathrm{UniformOnFun.ofFun}\\,𝔖 \\circ \\mathrm{DFunLike.coe}\\right)$$$

Lean4

theorem isUniformInducing_coeFn [UniformSpace F] [IsUniformAddGroup F] (𝔖 : Set (Set E)) :
    IsUniformInducing (α := UniformConvergenceCLM σ F 𝔖) (UniformOnFun.ofFun 𝔖 ∘ DFunLike.coe) :=
  ⟨rfl⟩

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