insert_union

Mathlib.Data.Finset.Lattice.Lemmas

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

English

insert a (s ∪ t) = insert a s ∪ insert a t.

Русский

insert a (s ∪ t) = insert a s ∪ insert a t.

LaTeX

$$$\\mathrm{insert}\\ a\\ (s \\cup t) = (\\mathrm{insert}\\ a\\ s) \\cup (\\mathrm{insert}\\ a\\ t)$$$

Lean4

@[simp, grind =]
theorem insert_union (a : α) (s t : Finset α) : insert a s ∪ t = insert a (s ∪ t) := by
  simp only [insert_eq, union_assoc]

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

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

Разделы

Аффилиация

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