pi — Mathlib · SciLib

English

From a family of continuous linear maps f_i: M → L[R] φ_i, one obtains a continuous linear map pi f: M → L[R] ∀i, φ_i sending x to (f_i x)_i.

Русский

Из семейства непрерывных линейных отображений f_i: M → φ_i получается отображение-«пи» pi f: M → ∀i, φ_i, отправляющее x в кортеж (f_i(x))_i.

LaTeX

$$$\\pi f (x) = (f_i(x))_{i\\in I}$$$

Lean4

/-- `pi` construction for continuous linear functions. From a family of continuous linear functions
it produces a continuous linear function into a family of topological modules. -/
def pi (f : ∀ i, M →L[R] φ i) : M →L[R] ∀ i, φ i :=
  ⟨LinearMap.pi fun i => f i, continuous_pi fun i => (f i).continuous⟩

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