English
If every function in l: List (α → α) is injective, and f: α → α is injective, then the composition folded by l via Function.comp is injective: foldl Function.comp f l is injective.
Русский
Если все функции в списке l: List (α → α) взаимно инъективны, и f: α → α инъективна, то свёртка по списку через композицию Function.comp даёт инъективную функцию: foldl Function.comp f l инъективна.
LaTeX
$$$$\text{If } l:\ List(\alpha\to\alpha),\ \big(\forall g\in l,\text{Injective}(g)\big),\ \text{Injective}(f) \Rightarrow \text{Injective}(\operatorname{foldl} (\text{Function.comp})\ f\ l).$$$$
Lean4
theorem injective_foldl_comp {l : List (α → α)} {f : α → α} (hl : ∀ f ∈ l, Function.Injective f)
(hf : Function.Injective f) : Function.Injective (@List.foldl (α → α) (α → α) Function.comp f l) := by
induction l generalizing f with
| nil => exact hf
| cons lh lt l_ih =>
apply l_ih fun _ h => hl _ (List.mem_cons_of_mem _ h)
apply Function.Injective.comp hf
apply hl _ mem_cons_self
