le_iff_disjoint_sdiff

Mathlib.Order.BooleanAlgebra.Basic

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

English

If hd is disjoint x z, hz: z ≤ y, hs: y ≤ x ⊔ z, then y \ x = z.

Русский

Если hd : Disjoint x z, hz: z ≤ y, hs: y ≤ x ⊔ z, тогда y \ x = z.

LaTeX

$$$\text{Disjoint } x z \rightarrow (z \le y) \rightarrow (y \le x \lor z) \Rightarrow y \setminus x = z$$$

Lean4

theorem le_iff_disjoint_sdiff (hz : z ≤ y) (hx : x ≤ y) : z ≤ x ↔ Disjoint z (y \ x) :=
  (disjoint_sdiff_iff_le hz hx).symm

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

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

Разделы

Аффилиация

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