restriction — Mathlib

English

The restriction of an algebra norm to a subalgebra is again an algebra norm on that subalgebra.

Русский

Ограничение алгебраической нормы на подалгебру снова является нормой этой подалгебры.

LaTeX

$$$restriction(A\\,f) : AlgebraNorm\\,R\\,A$$$

Lean4

/-- The restriction of an algebra norm to a subalgebra. -/
def restriction (A : Subalgebra R S) (f : AlgebraNorm R S) : AlgebraNorm R A
    where
  toFun x := f x.val
  map_zero' := map_zero f
  add_le' x y := map_add_le_add _ _ _
  neg' x := map_neg_eq_map _ _
  mul_le' x y := map_mul_le_mul _ _ _
  eq_zero_of_map_eq_zero' x hx := by rw [← ZeroMemClass.coe_eq_zero]; exact eq_zero_of_map_eq_zero f hx
  smul' r x := map_smul_eq_mul _ _ _

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