disjoint_sup_left — Mathlib

English

In a distributive lattice with bottom, Disjoint (a ⊔ b) c holds iff Disjoint a c and Disjoint b c.

Русский

В распределительной решетке с нулем, несовместимость (a ⊔ b) с c эквивалентна несовместимости a с c и несовместимости b с c.

LaTeX

$$$Disjoint (a \sqcup b) c \iff (Disjoint a c) \land (Disjoint b c)$$$

Lean4

@[simp]
theorem disjoint_sup_left : Disjoint (a ⊔ b) c ↔ Disjoint a c ∧ Disjoint b c := by
  simp only [disjoint_iff, inf_sup_right, sup_eq_bot_iff]

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