normedAddCommGroup — Mathlib

English

There is a normed additive commutative group structure on e.finiteSubspace given by x ↦ e(x) as its norm and the inherited metric.

Русский

На e.finiteSubspace задаётся нормированная абелева группа через x ↦ e(x) как норму и унаследованную метрику.

LaTeX

$$instance normedAddCommGroup : NormedAddCommGroup e.finiteSubspace := { norm := fun x => (e x).toReal, dist_eq := fun _ _ => rfl }$$

Lean4

/-- Normed group instance on `e.finiteSubspace`. -/
instance normedAddCommGroup : NormedAddCommGroup e.finiteSubspace :=
  { e.metricSpace with
    norm := fun x => (e x).toReal
    dist_eq := fun _ _ => rfl }

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