singleton_disjiUnion

Mathlib.Data.Finset.Union

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

English

The disjiUnion over a singleton {a} is just t(a).

Русский

DisjiUnion для синглтона {a} равно t(a).

LaTeX

$$$ Finset.disjiUnion\\{a\\} t = t(a) $$$

Lean4

@[simp]
theorem singleton_disjiUnion (a : α) {h} : Finset.disjiUnion { a } t h = t a :=
  eq_of_veq <| Multiset.singleton_bind _ _

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

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

Разделы

Аффилиация

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