image_prodMk_subset_prod — Mathlib

English

The image of s under x ↦ (f x, g x) is contained in the product of the images of s under f and g.

Русский

Образ отображения x ↦ (f x, g x) множества s содержится в произведении образов f(s) и g(s).

LaTeX

$$$ (f \times g)'' s \subseteq (f'' s) \times (g'' s) $$$

Lean4

theorem image_prodMk_subset_prod {f : α → β} {g : α → γ} {s : Set α} :
    (fun x => (f x, g x)) '' s ⊆ (f '' s) ×ˢ (g '' s) := by grind

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