English
Let s ⊆ α, t ⊆ β, f: α → β → γ, g: γ → Set δ. Then ⋃ c ∈ image2 f s t, g c equals ⋃ a ∈ s, ⋃ b ∈ t, g(f a b).
Русский
Пусть s ⊆ α, t ⊆ β, f: α → β → γ, g: γ → Set δ. Тогда ⋃ c ∈ image2 f s t, g c = ⋃ a ∈ s, ⋃ b ∈ t, g(f a b).
LaTeX
$$$\bigcup_{c \in \operatorname{image2} f s t} g(c) = \bigcup_{a \in s} \bigcup_{b \in t} g(f(a,b))$$$
Lean4
theorem biUnion_image2 (s : Set α) (t : Set β) (f : α → β → γ) (g : γ → Set δ) :
⋃ c ∈ image2 f s t, g c = ⋃ a ∈ s, ⋃ b ∈ t, g (f a b) :=
iSup_image2 ..