mk_preimage_prod — Mathlib

English

Let f: γ → α, g: γ → β. Then the preimage of s × t under the map x ↦ (f x, g x) equals the intersection f^{-1}(s) ∩ g^{-1}(t).

Русский

Пусть f: γ → α, g: γ → β. Тогда (f × g)^{-1}(s × t) = f^{-1}(s) ∩ g^{-1}(t).

LaTeX

$$$ (f^{-1}(s)) \cap (g^{-1}(t)) = (\lambda x:\gamma, (f x, g x))^{-1}(s \times t) $$$

Lean4

theorem mk_preimage_prod (f : γ → α) (g : γ → β) : (fun x => (f x, g x)) ⁻¹' s ×ˢ t = f ⁻¹' s ∩ g ⁻¹' t :=
  rfl

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