preimage_prod_map_prod — Mathlib

English

For f: α → β, g: γ → δ and sets s ⊆ β, t ⊆ δ, the preimage of s × t under the product map Prod.map f g equals f^{-1}(s) × g^{-1}(t).

Русский

Для отображений f: α → β, g: γ → δ и множеств s ⊆ β, t ⊆ δ верно: (Prod.map f g)^{-1}(s × t) = f^{-1}(s) × g^{-1}(t).

LaTeX

$$$ (Prod.map f g)^{-1}(s \times t) = f^{-1}(s) \times g^{-1}(t) $$$

Lean4

theorem preimage_prod_map_prod (f : α → β) (g : γ → δ) (s : Set β) (t : Set δ) :
    Prod.map f g ⁻¹' s ×ˢ t = (f ⁻¹' s) ×ˢ (g ⁻¹' t) :=
  rfl

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