mem_Icc_iff_norm_le_one — Mathlib

English

An element lies in the interval [0,1] exactly when it is nonnegative and has norm at most 1.

Русский

Элемент лежит в интервале [0,1], если и только если он неотрицателен и его норма не превышает 1.

LaTeX

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

Lean4

theorem mem_Icc_iff_norm_le_one {x : A} : x ∈ Icc 0 1 ↔ 0 ≤ x ∧ ‖x‖ ≤ 1 := by
  simpa only [map_one] using mem_Icc_algebraMap_iff_norm_le zero_le_one (A := A)

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