disjoint_of_erase_right

Mathlib.Data.Finset.Basic

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

← MathLib Explorer

English

If a ∉ s and Disjoint s (t \\ {a}), then Disjoint s t.

Русский

Если a ∉ s и Disjoint s (t \\ {a}), тогда Disjoint s t.

LaTeX

$$$ (ha : a \\notin s) (hst : Disjoint s (t \\ {a})) : Disjoint s t$$$

Lean4

theorem disjoint_of_erase_right (ha : a ∉ s) (hst : Disjoint s (t.erase a)) : Disjoint s t :=
  by
  rw [← erase_insert ha, disjoint_erase_comm, disjoint_insert_left]
  exact ⟨notMem_erase _ _, hst⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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