map_iterate — Mathlib

English

For all n, the n-th iterate of Prod.map f g equals Prod.map (f^n) (g^n) (i.e., Nat.iterate).

Русский

Для любого n тождество: n-й повтор разложения Prod.map f g равен Prod.map (f^n) (g^n).

LaTeX

$$$\\operatorname{Nat.iterate}(\\\\operatorname{Prod.map} f g) n = \\\\operatorname{Prod.map}(\\\\operatorname{Nat.iterate} f n)(\\\\operatorname{Nat.iterate} g n).$$$

Lean4

@[simp]
theorem map_iterate (f : α → α) (g : β → β) (n : ℕ) : (Prod.map f g)^[n] = Prod.map f^[n] g^[n] := by
  induction n <;> simp [*, Prod.map_comp_map]

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