disjoint_inf_sdiff

Mathlib.Order.BooleanAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#disjoint_inf_sdiff

English

In a generalized Boolean algebra, the meet of x and y is disjoint from x \ y; i.e., (x ∧ y) ∧ (x \ y) = ⊥.

Русский

В обобщённой булевой алгебре встреча x и y несовпадает с разностью x \ y; то есть (x ∧ y) ∧ (x \ y) = ⊥.

LaTeX

$$$(x \wedge y) \wedge (x \setminus y) = \bot$$$

Lean4

theorem disjoint_inf_sdiff : Disjoint (x ⊓ y) (x \ y) :=
  disjoint_iff_inf_le.mpr (inf_inf_sdiff x y).le

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

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

Разделы

Аффилиация

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