instNorm — Mathlib

English

The norm on a quotient M ⧸ S is defined as the infimum of the norm on representatives, i.e., ‖x̄‖ = inf{‖m‖ : m ∈ M, m ∈ x̄}.

Русский

Норма на фактор-группе M ⧸ S задаётся как инфимум норм представителей: ∥x̄∥ = inf{∥m∥ : m ∈ M, m̄ = x̄}.

LaTeX

$$$\|\overline{m}\| = \inf\{ \|m'\| : m' ∈ M, \; m' \text{ represents } \overline{m} \}$$$

Lean4

/-- The norm of `x` on the quotient by a subgroup `S` is defined as the infimum of the norm on
`x * S`. -/
@[to_additive /-- The norm of `x` on the quotient by a subgroup `S` is defined as the infimum of the norm on
    `x + S`. -/
    ]
noncomputable instance instNorm : Norm (M ⧸ S) where norm := groupSeminorm

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