posPart_one

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic

URI: https://scilib.ai/kg/mathlib#CFC.posPart_one

English

The positive part of the unit element is the unit itself, i.e., (1)⁺ = 1.

Русский

Положительная часть единицы равна самой единице: (1)⁺ = 1.

LaTeX

$$$1^+ = 1$$$

Lean4

@[simp]
theorem posPart_one : (1 : A)⁺ = 1 := by
  rw [CFC.posPart_def, cfcₙ_eq_cfc]
  simp

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

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

Разделы

Аффилиация

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