prodMap — Mathlib

English

If MapsTo f1 s1 t1 and MapsTo f2 s2 t2, then MapsTo (fun x => (f1 x.1, f2 x.2)) (s1 ×ˢ s2) (t1 ×ˢ t2).

Русский

Если отображения f1 и f2 переводят s1 в t1 и s2 в t2 соответственно, то отображение пары переводит s1 × s2 в t1 × t2.

LaTeX

$$$ \\operatorname{MapsTo} f1 s1 t1 \\Rightarrow \\operatorname{MapsTo} f2 s2 t2 \\Rightarrow \\operatorname{MapsTo} (fun x \\mapsto { fst := f1 x.fst, snd := f2 x.snd }) (s1 \\timesˢ s2) (t1 \\timesˢ t2). $$$

Lean4

theorem prodMap (h₁ : MapsTo f₁ s₁ t₁) (h₂ : MapsTo f₂ s₂ t₂) :
    MapsTo (fun x ↦ (f₁ x.1, f₂ x.2)) (s₁ ×ˢ s₂) (t₁ ×ˢ t₂) := fun _x hx ↦ ⟨h₁ hx.1, h₂ hx.2⟩

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