disjoint_sup_right — Mathlib

English

In a distributive lattice with bottom, Disjoint (a ⊔ b) c is equivalent to (Disjoint a c) ∧ (Disjoint b c) (simplified form).

Русский

В распределительной решетке с нулем, несовместимость (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_right : Disjoint a (b ⊔ c) ↔ Disjoint a b ∧ Disjoint a c := by
  simp only [disjoint_iff, inf_sup_left, sup_eq_bot_iff]

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