singleton_sups_singleton — Mathlib

English

The image of a join of finite sets under a map distributes over the join: image(f, s ⊻ t) = image(f, s) ⊻ image(f, t).

Русский

Образ суммы по функции распространяется на сумму: image(f, s ⊻ t) = image(f, s) ⊻ image(f, t).

LaTeX

$$$\mathrm{image}(f, s \oplus t) = \mathrm{image}(f, s) \oplus \mathrm{image}(f, t)$$$

Lean4

theorem singleton_sups_singleton : ({ a } ⊻ { b } : Finset α) = {a ⊔ b} :=
  image₂_singleton

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