mem_Icc_iff_nnnorm_le_one

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

URI: https://scilib.ai/kg/mathlib#CStarAlgebra.mem_Icc_iff_nnnorm_le_one

English

In A, x ∈ [0,1] if and only if 0 ≤ x and ‖x‖₊ ≤ 1.

Русский

В A: x ∈ [0,1] эквивалентно 0 ≤ x и ‖x‖₊ ≤ 1.

LaTeX

$$x ∈ Icc 0 1 \\iff 0 ≤ x ∧ ‖x‖₊ ≤ 1$$

Lean4

theorem mem_Icc_iff_nnnorm_le_one {x : A} : x ∈ Icc 0 1 ↔ 0 ≤ x ∧ ‖x‖₊ ≤ 1 :=
  mem_Icc_iff_norm_le_one

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru