prod_preimage_right — Mathlib

English

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

Русский

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

LaTeX

$$$ s \timesˢ (g^{-1}(t)) = (\text{fun } p : α × δ => (p.1, g p.2))^{-1}(s × t) $$$

Lean4

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

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