coe_sup

Mathlib.Analysis.NormedSpace.MStructure

URI: https://scilib.ai/kg/mathlib#IsLprojection.coe_sup

English

The value of the supremum of P and Q, when projected to M, equals the ambient value P + Q − P Q.

Русский

Значение верхней границы P и Q при отображении в M равно P+Q−PQ.

LaTeX

$$Eq $(P\\lor Q).val = P.val + Q.val - P.val \\cdot Q.val$.$$

Lean4

@[simp]
theorem coe_sup [FaithfulSMul M X] (P Q : { P : M // IsLprojection X P }) : ↑(P ⊔ Q) = (↑P : M) + ↑Q - ↑P * ↑Q :=
  rfl

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

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

Разделы

Аффилиация

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