disjoint_of_erase_left

Mathlib.Data.Finset.Basic

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

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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