biUnion_image_sup_right — Mathlib

English

The image of a product under the uncurry sup map equals the sups of images: image((uncurry ⊔)) (s × t) = s ⊻ t.

Русский

Образ произведения под отображением ⊔ через uncurry равен сумме образов: image((uncurry ⊔)) (s × t) = s ⊻ t.

LaTeX

$$$\mathrm{image}(\mathrm{uncurry}(\lambda x y \mapsto x \sqcup y), s \times t) = s \oplus t$$$

Lean4

theorem biUnion_image_sup_right : t.biUnion (fun b ↦ s.image (· ⊔ b)) = s ⊻ t :=
  biUnion_image_right

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