prod_preimage_left — Mathlib

English

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

Русский

Для отображения f: γ → α и множеств s ⊆ α, t ⊆ β верно: (f^{-1}(s)) × t = (f × id)^{-1}(s × t) под отображением (p, b) ↦ (f p, b).

LaTeX

$$$ (f^{-1}(s)) \timesˢ t = (\text{fun } p : \gamma \times \beta \Rightarrow (f p.1, p.2))^{-1}(s \times t) $$$

Lean4

theorem prod_preimage_left {f : γ → α} : (f ⁻¹' s) ×ˢ t = (fun p : γ × β => (f p.1, p.2)) ⁻¹' s ×ˢ t :=
  rfl

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