max_le_prod_norm — Mathlib

English

One can furnish a normed additive commutative group structure on C⋆ᵐᵒᵈ(A, E×F) by transferring the core from the base C*-module structure.

Русский

Можно задать нормированную аддитивную коммутативную группу на C⋆ᵐᵒᵈ(A, E×F) перенеся ядро из базовой структуры C*-модуля.

LaTeX

$$$\\text{normedAddCommGroupProdAux}:= \\text{NormedAddCommGroup.ofCore (CStarModule.normedSpaceCore A)}$$$

Lean4

theorem max_le_prod_norm (x : C⋆ᵐᵒᵈ(A, E × F)) : max ‖x.1‖ ‖x.2‖ ≤ ‖x‖ :=
  by
  rw [prod_norm]
  simp only [norm_eq_sqrt_norm_inner_self (A := A) (E := E), norm_eq_sqrt_norm_inner_self (A := A) (E := F), max_le_iff,
    norm_nonneg, Real.sqrt_le_sqrt_iff]
  constructor
  all_goals
    refine CStarAlgebra.norm_le_norm_of_nonneg_of_le (A := A) ?_ ?_
    all_goals aesop (add safe apply CStarModule.inner_self_nonneg)

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