norm_equiv_le_norm_prod — Mathlib

English

The norm on the equivalence class via equiv equals the norm in the product module: ||equiv x|| ≤ ||x||.

Русский

Норма класса эквивалентности через эквив использует норму в произведении: ||equiv x|| ≤ ||x||.

LaTeX

$$$\\forall x:\\, C⋆ᵐᵒᵈ(A, E \\times F), \\|equiv(A,(E\\times F))\,x\\| \\leq \\|x\\|$$$

Lean4

theorem norm_equiv_le_norm_prod (x : C⋆ᵐᵒᵈ(A, E × F)) : ‖equiv A (E × F) x‖ ≤ ‖x‖ :=
  max_le_prod_norm x

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