iUnion_image_sup_right

Mathlib.Data.Set.Sups

URI: https://scilib.ai/kg/mathlib#Set.iUnion_image_sup_right

English

Union over right index equals sups: ⋃ b ∈ t, (· ⊔ b) '' s = s ⊻ t.

Русский

Объединение по правому индексу даёт супс: ⋃ b ∈ t, (· ⊔ b) '' s = s ⊻ t.

LaTeX

$$$ \\bigcup_{b \\in t} \\{ a \\uplus b \mid a \in s \\} = s \\veebar t $$$

Lean4

theorem iUnion_image_sup_right : ⋃ b ∈ t, (· ⊔ b) '' s = s ⊻ t :=
  iUnion_image_right _

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

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

Разделы

Аффилиация

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