isUniformInducing_toUniformOnFun — Mathlib

English

Describes the range of toUniformOnFun again, emphasizing the equivalence of the construction with the topological structure on uniform-on-fun maps.

Русский

Еще одно описание диапазона toUniformOnFun, подчеркивающее эквивалентность конструкции с топологией на uniform-on-fun отображениях.

LaTeX

$$$\text{range}(\text{toUniformOnFun}) = \{ f : (Π i, E_i) →ᵤ[...] F \mid \dots \}$$$

Lean4

theorem isUniformInducing_toUniformOnFun :
    IsUniformInducing (toUniformOnFun : ContinuousMultilinearMap 𝕜 E F → ((Π i, E i) →ᵤ[{s | IsVonNBounded 𝕜 s}] F)) :=
  ⟨rfl⟩

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