range_prodMap — Mathlib

English

The range of Prod.map f g is equal to the product of the ranges: range (Prod.map f g) = range f × range g.

Русский

Образ отображения Prod.map f g равен произведению образов: range (Prod.map f g) = range f × range g.

LaTeX

$$$ range (Prod.map f g) = range f \timesˢ range g $$$

Lean4

@[simp, mfld_simps]
theorem range_prodMap {m₁ : α → γ} {m₂ : β → δ} : range (Prod.map m₁ m₂) = range m₁ ×ˢ range m₂ :=
  prod_range_range_eq.symm

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