preimage_inr_Icc_zero_one

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

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

← MathLib Explorer

English

For x ∈ A, the membership of (x : A⁺¹) in Icc 0 1 is equivalent to 0 ≤ x and ∥x∥ ≤ 1.

Русский

Для x ∈ A принадлежность (x) в Icc 0 1 эквивалентна 0 ≤ x и ∥x∥ ≤ 1.

LaTeX

$$$(x: A)\\in Icc(0,1) \\iff 0 \\le x \\wedge \\|x\\| \\le 1.$$$

Lean4

theorem preimage_inr_Icc_zero_one : ((↑) : A → A⁺¹) ⁻¹' Icc 0 1 = {x : A | 0 ≤ x} ∩ closedBall 0 1 :=
  by
  ext
  simp [-mem_Icc, inr_mem_Icc_iff_norm_le]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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