inter_insert_of_notMem

Mathlib.Data.Finset.Lattice.Lemmas

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

← MathLib Explorer

English

If a ∉ S2, then S1 ∩ (S2 ∪ {a}) = S1 ∩ S2.

Русский

Если a не принадлежит S2, то S1 ∩ (S2 ∪ {a}) = S1 ∩ S2.

LaTeX

$$$a \notin S_2 \Rightarrow S_1 \cap (S_2 \cup \{a\}) = S_1 \cap S_2$$$

Lean4

@[simp]
theorem inter_insert_of_notMem {s₁ s₂ : Finset α} {a : α} (h : a ∉ s₁) : s₁ ∩ insert a s₂ = s₁ ∩ s₂ := by
  rw [inter_comm, insert_inter_of_notMem h, inter_comm]

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

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

Разделы

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

Аффилиация

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