prod_image_image_eq — Mathlib

English

The product of the images (m1''s) and (m2''t) equals the image of s×t under the map p ↦ (m1 p.1, m2 p.2).

Русский

Произведение изображений m1''S и m2''T равно образу множества S×T под отображением p ↦ (m1 p.1, m2 p.2).

LaTeX

$$$ (m_1'' s) \timesˢ (m_2'' t) = \left( p \mapsto (m_1 p.1, m_2 p.2) \right)'' (s \timesˢ t) $$$

Lean4

theorem prod_image_image_eq {m₁ : α → γ} {m₂ : β → δ} :
    (m₁ '' s) ×ˢ (m₂ '' t) = (fun p : α × β => (m₁ p.1, m₂ p.2)) '' s ×ˢ t :=
  ext <| by simp [-exists_and_right, exists_and_right.symm, and_left_comm, and_assoc, and_comm]

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