foldr'_ι — Mathlib

English

A second auxiliary relation shows compatibility between foldr' and the next-layer foldr'Aux, ensuring coherence of the two-tier recursion for all generators m and x.

Русский

Вторая вспомогательная связка демонстрирует совместимость между foldr' и foldr'Aux, обеспечивая согласованность двухуровневой рекурсии по всем генераторам m и x.

LaTeX

$$$foldr'Aux\\ Q\\ f\\ hf\\ n\\ (ι_Q m) = f m (1, n)$$$

Lean4

theorem foldr'_ι (f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N) (hf : ∀ m x fx, f m (ι Q m * x, f m (x, fx)) = Q m • fx)
    (n m) : foldr' Q f hf n (ι Q m) = f m (1, n) :=
  congr_arg Prod.snd (foldr_ι _ _ _ _ _)

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