English
If range f is contained in range g, then for any a, the range of foldr f a is contained in the range of foldr g a.
Русский
Если диапазон f вложен в диапазон g, то для любого a множество значений foldr f a вложено в множество значений foldr g a.
LaTeX
$$$\\forall {\\\\alpha} {\\\\beta} {\\\\gamma} {f : \\\\beta \\\\rightarrow \\\\alpha \\\\rightarrow \\\\alpha} {g : \\\\gamma \\\\rightarrow \\\\alpha \\\\rightarrow \\\\alpha},\n Set.range f ⊆ Set.range g \\\\rightarrow \\\\forall a : \\\\alpha, Set.range (List.foldr f a) ⊆ Set.range (List.foldr g a)$$$
Lean4
theorem foldr_range_subset_of_range_subset {f : β → α → α} {g : γ → α → α} (hfg : Set.range f ⊆ Set.range g) (a : α) :
Set.range (foldr f a) ⊆ Set.range (foldr g a) :=
by
rintro _ ⟨l, rfl⟩
induction l with
| nil => exact ⟨[], rfl⟩
| cons b l H =>
obtain ⟨c, hgf⟩ := hfg (Set.mem_range_self b)
obtain ⟨m, hgf'⟩ := H
rw [foldr_cons, ← hgf, ← hgf']
exact ⟨c :: m, rfl⟩
