instMulNorm — Mathlib

English

There is a norm on SeparationQuotient E induced by lifting the norm on E; the norm is compatible with the quotient structure.

Русский

Существует норма на SeparationQuotient E, полученная по подъемному контуру нормы на E; норма согласована с факторной структурой.

LaTeX

$$$\\text{Norm}(\\text{SeparationQuotient } E) = \\mathrm{lift}\\; \\text{Norm}.\\norm$$$

Lean4

@[to_additive instNorm]
instance instMulNorm : Norm (SeparationQuotient E) where norm := lift Norm.norm fun _ _ h => h.norm_eq_norm'

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