English
Let f: γ → α, g: δ → β be functions and s ⊆ α, t ⊆ β. Then the Cartesian product of the preimages equals the preimage under the product map (p, q) ↦ (f p, g q); i.e., (f^{-1}(s)) × (g^{-1}(t)) = (f × g)^{-1}(s × t).
Русский
Пусть f: γ → α, g: δ → β — отображения, и s ⊆ α, t ⊆ β. Тогда произведение предобразов по отдельным координатам равно предобразу по произведению функций: (f^{-1}(s)) × (g^{-1}(t)) = (f × g)^{-1}(s × t).
LaTeX
$$$ (f^{-1}(s)) \times (g^{-1}(t)) = (f \\times g)^{-1}(s \\times t) $$$
Lean4
theorem prod_preimage_eq {f : γ → α} {g : δ → β} :
(f ⁻¹' s) ×ˢ (g ⁻¹' t) = (fun p : γ × δ => (f p.1, g p.2)) ⁻¹' s ×ˢ t :=
rfl
