disjoint_insert_erase

Mathlib.Data.Finset.Basic

URI: https://scilib.ai/kg/mathlib#Finset.disjoint_insert_erase

English

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

Русский

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

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru