biUnion_val

Mathlib.Data.Finset.Union

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

English

The underlying multiset of a biUnion is the deduplicated bind of the fibres.

Русский

Основание biUnion — это dedup связанного множества волокон.

LaTeX

$$$(s.biUnion t).1 = (s.1.bind (\\lambda a => (t a).1)).dedup$$$

Lean4

@[simp]
theorem biUnion_val (s : Finset α) (t : α → Finset β) : (s.biUnion t).1 = (s.1.bind fun a ↦ (t a).1).dedup :=
  rfl

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

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

Разделы

Аффилиация

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