coe_sdiff

Mathlib.Analysis.NormedSpace.MStructure

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

English

The operation sdiff on the subtype corresponds to the ambient algebra expression $P(1-Q)$.

Русский

Операция sdiff на подтипе соответствует выражению $P(1-Q)$ в пространстве $M$.

LaTeX

$$$\\uparrow(P \\setminus Q) = (\\uparrow P) \\cdot (1 - \\uparrow Q)$$$

Lean4

@[simp]
theorem coe_sdiff [FaithfulSMul M X] (P Q : { P : M // IsLprojection X P }) : ↑(P \ Q) = (↑P : M) * (1 - ↑Q) :=
  rfl

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

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

Разделы

Аффилиация

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