biUnion_image_sup_left

Mathlib.Data.Finset.Sups

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

English

A biunion on the right distributes over a family: t.biUnion (a ↦ s.image (· ⊔ a)) = s ⊻ t.

Русский

Биобъединение справа распределяется над множестом: t.biUnion (a ↦ s.image (· ⊔ a)) = s ⊻ t.

LaTeX

$$$t \mathrm{biUnion} (a \mapsto s.image (· ⊔ a)) = s ⊻ t$$$

Lean4

theorem biUnion_image_sup_left : s.biUnion (fun a ↦ t.image (a ⊔ ·)) = s ⊻ t :=
  biUnion_image_left

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

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

Разделы

Аффилиация

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