normOneClass — Mathlib

English

If ι is a finite nonempty type and each α i has NormOneClass, then the space of functions ∀ i, α i has NormOneClass.

Русский

Если ι конечен и не пуст, и для каждого i пространства α i имеет NormOneClass, то пространство функций ∀ i, α i имеет NormOneClass.

LaTeX

$$$\text{NormOneClass}(\forall i:\, ι,\ α(i)).$$$

Lean4

instance normOneClass {ι : Type*} {α : ι → Type*} [Nonempty ι] [Fintype ι] [∀ i, SeminormedAddCommGroup (α i)]
    [∀ i, One (α i)] [∀ i, NormOneClass (α i)] : NormOneClass (∀ i, α i) :=
  ⟨by simpa [Pi.norm_def] using Finset.sup_const Finset.univ_nonempty 1⟩

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