sup

Mathlib.Analysis.NormedSpace.MStructure

URI: https://scilib.ai/kg/mathlib#IsLprojection.Subtype.sup

English

The supremum construction for L-projections is implemented by max with the formula P+Q−PQ.

Русский

Построение верхней границы для L-проекций реализуется формулой P+Q−PQ.

LaTeX

$$Join of $P$ and $Q$ as an L-projection is $P+Q-PQ$.$$

Lean4

instance sup [FaithfulSMul M X] : Max { P : M // IsLprojection X P } :=
  ⟨fun P Q => ⟨P + Q - P * Q, P.prop.join Q.prop⟩⟩

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

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

Разделы

Аффилиация

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