inr_mem_Icc_iff_norm_le — Mathlib

English

For any x in A, membership of its image in the unitized algebra inside the interval [0,1] corresponds to 0 ≤ x and the norm of x bounded by 1.

Русский

Для любого x в A членство образа x в единичной нормированной алгебре внутри интервала [0,1] эквивалентно 0 ≤ x и нормa x не превосходит 1.

LaTeX

$$$(x: A^{+1}) \\in [0,1] \\text{ iff } 0 \\le x \\text{ and } \\|x\\| \\le 1.$$$

Lean4

theorem inr_mem_Icc_iff_norm_le {x : A} : (x : A⁺¹) ∈ Icc 0 1 ↔ 0 ≤ x ∧ ‖x‖ ≤ 1 :=
  by
  simp only [mem_Icc, inr_nonneg_iff, and_congr_right_iff]
  rw [← norm_inr (𝕜 := ℂ), ← inr_nonneg_iff, iff_comm]
  exact (norm_le_one_iff_of_nonneg _ ·)

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