English
For f: α' → β' → γ, g: α → α' and h: β → β', the image of the product range is the range of the composed map (x,y) ↦ f(g x, h y). In symbols: image2 f (range g) (range h) = range (λ x : α × β, f (g x.1) (h x.2)).
Русский
Для отображения f: α' → β' → γ, отображения g: α → α' и h: β → β' верная картинка образа произведения равна образу композиции (x,y) ↦ f(g x, h y). То есть image2 f (range g) (range h) = range (λ x : α × β, f (g x.1) (h x.2)).
LaTeX
$$$\\operatorname{image}_2 f (\\operatorname{range} g) (\\operatorname{range} h) = \\operatorname{range} (\\lambda x : \\alpha \\times \\beta.\\ f (g x.1) (h x.2))$$$
Lean4
theorem image2_range (f : α' → β' → γ) (g : α → α') (h : β → β') :
image2 f (range g) (range h) = range fun x : α × β ↦ f (g x.1) (h x.2) := by
simp_rw [← image_univ, image2_image_left, image2_image_right, ← image_prod, univ_prod_univ]
