biUnion_image2 — Mathlib

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 ..

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