image_sup_prod

Mathlib.Data.Set.Sups

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

English

The image of a join over s and t equals the join of the images: image2 (⊔) s t = s ⊻ t.

Русский

Образ объединения по верхам равен объединению образов: image2 (⊔) s t = s ⊻ t.

LaTeX

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

Lean4

@[simp]
theorem image_sup_prod (s t : Set α) : Set.image2 (· ⊔ ·) s t = s ⊻ t :=
  rfl

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

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

Разделы

Аффилиация

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