sigma — Mathlib

English

The construction sigma on SeminormFamily aggregates a family of seminorms into a single seminorm family over a product index, by listing the pair (i, κ_i) as the index set.

Русский

Конструкция сигма для семейства семинорм объединяет семейство семинорм в единое семинормное семейство над произведённым индексом (пара i, κ_i).

LaTeX

$$$ SeminormFamily.sigma \\ (p) : SeminormFamily 𝕜 E ((i : \\mathbb{I}) × κ i) $$$

Lean4

/-- (Disjoint) union of seminorm families. -/
protected def sigma {κ : ι → Type*} (p : (i : ι) → SeminormFamily 𝕜 E (κ i)) : SeminormFamily 𝕜 E ((i : ι) × κ i) :=
  fun ⟨i, k⟩ => p i k

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