prod_ofNat_val — Mathlib

English

The nth element of α × β corresponds to the pair of nth elements of α and β obtained via unpair.

Русский

n-й элемент α × β соответствует паре из n-й элемента α и n-й элемента β, полученной через unpair.

LaTeX

$$$ \operatorname{ofNat}(\alpha \times \beta)\ n = \big( \operatorname{ofNat} \alpha (\mathrm{unpair}(n).1), \operatorname{ofNat} \beta (\mathrm{unpair}(n).2) \big) $$$

Lean4

theorem prod_ofNat_val (n : ℕ) : ofNat (α × β) n = (ofNat α (unpair n).1, ofNat β (unpair n).2) := by simp

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