pair_preimage — Mathlib

English

The preimage of a product set s × t under pair f g equals the intersection of the preimages: f^{-1} s ∩ g^{-1} t.

Русский

Предобраз произведения множеств s × t под pair f g равен пересечению предобразов: f^{-1} s ∩ g^{-1} t.

LaTeX

$$$$ pair\\, f\\, g^{-1}'(s \\times\\!\\! t) = f^{-1}'s \\cap g^{-1}'t. $$$$

Lean4

theorem pair_preimage (f : α →ₛ β) (g : α →ₛ γ) (s : Set β) (t : Set γ) : pair f g ⁻¹' s ×ˢ t = f ⁻¹' s ∩ g ⁻¹' t :=
  rfl

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