disjoint_erase_insert — Mathlib

English

If a is not in s, then Disjoint (insert a s) (t \\ {a}) is equivalent to Disjoint s t.

Русский

Если a не принадлежит s, то Disjoint (insert a s) (t \\ {a}) эквивалентно Disjoint s t.

LaTeX

$$$ (ha : a \\notin s) \\Rightarrow (Disjoint (insert a s) (t \\ {a}) \\iff Disjoint s t)$$$

Lean4

theorem disjoint_erase_insert (ha : a ∉ s) : Disjoint (insert a s) (t.erase a) ↔ Disjoint s t := by
  rw [← disjoint_erase_comm, erase_insert ha]

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