disjoint_insert_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem disjoint_insert_right : Disjoint s (insert a t) ↔ a ∉ s ∧ Disjoint s t :=
  disjoint_comm.trans <| by rw [disjoint_insert_left, _root_.disjoint_comm]

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