inter_insert_of_mem

Mathlib.Data.Finset.Lattice.Lemmas

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

← MathLib Explorer

English

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

Русский

Если a ∈ S1, то S1 ∩ (S2 ∪ {a}) = (S1 ∩ S2) ∪ {a}.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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