mem_Icc_algebraMap_iff_nnnorm_le — Mathlib

English

In the nonnegative real setting, membership in Icc 0 (algebraMap ℝ≥0 A r) is equivalent to 0 ≤ x and ‖x‖₊ ≤ r for r ∈ ℝ≥0.

Русский

В рамках неотрицательных вещественных чисел принадлежность x к Icc 0 (algebraMap ℝ≥0 A r) эквивалентна 0 ≤ x и ‖x‖₊ ≤ r для r ∈ ℝ≥0.

LaTeX

$$x ∈ Icc 0 (algebraMap ℝ≥0 A r) \\iff 0 \\le x ∧ ‖x‖₊ ≤ r$$

Lean4

theorem mem_Icc_algebraMap_iff_nnnorm_le {x : A} {r : ℝ≥0} : x ∈ Icc 0 (algebraMap ℝ≥0 A r) ↔ 0 ≤ x ∧ ‖x‖₊ ≤ r :=
  mem_Icc_algebraMap_iff_norm_le (hr := r.2)

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