proj — Mathlib

English

The projections from a family of topological modules are continuous linear maps: the i-th projection from ∏ φ_i to φ_i is linear and continuous.

Русский

Проекции из произведения семейства топологических модулей являются непрерывными линейными отображениями: i-я проекция из ∏ φ_i в φ_i линейна и непрерывна.

LaTeX

$$def proj (i) : (∀ i, φ i) →L[R] φ i := ⟨LinearMap.proj i, continuous_apply _⟩$$

Lean4

/-- The projections from a family of topological modules are continuous linear maps. -/
def proj (i : ι) : (∀ i, φ i) →L[R] φ i :=
  ⟨LinearMap.proj i, continuous_apply _⟩

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