instNormOneClass — Mathlib

English

The quotient by the separation relation inherits a NormOneClass from the base normed additive group.

Русский

Квотирование по разделению наследует NormOneClass от базовой нормированной аддитивной группы.

LaTeX

$$$ \\text{NormOneClass}(\\mathrm{SeparationQuotient}(\\alpha)) \\text{ with } \\|\\cdot\\| = \\|\\cdot\\|_\\alpha.$$$

Lean4

instance [SeminormedAddCommGroup α] [One α] [NormOneClass α] : NormOneClass (SeparationQuotient α) where
  norm_one := norm_one (α := α)

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