norm_ofSubsingleton_id — Mathlib

English

If ι is a subsingleton and G is nontrivial, then for any i in ι, the canonical map of that index has operator norm equal to 1.

Русский

При ι, являющимся единичной множеством, и непустого G, для любого i ∈ ι каноническое отображение индекса имеет норму 1.

LaTeX

$$$\|\operatorname{ofSubsingleton} \; 𝕜 \; G \; G \; i \; (\mathrm{id}_{G})\| = 1$$$

Lean4

theorem norm_ofSubsingleton_id [Subsingleton ι] [Nontrivial G] (i : ι) : ‖ofSubsingleton 𝕜 G G i (.id _ _)‖ = 1 := by
  simp

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