disjoint_insert_left — Mathlib

English

With decidable equality, Disjoint (insert a s) t is equivalent to a ∉ t and Disjoint s t.

Русский

При разрешимой эквивалентности вставка a в s сохраняет непересечение: Disjoint (insert a s) t ⇔ a ∉ t ∧ Disjoint s t.

LaTeX

$$$\\operatorname{Disjoint}(\\operatorname{insert}(a,s), t) \\iff (a \\notin t) \\land \\operatorname{Disjoint}(s,t)$$$

Lean4

@[simp]
theorem disjoint_insert_left : Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t := by
  simp only [disjoint_left, mem_insert, or_imp, forall_and, forall_eq]

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