English
Let f: α → β → α and g: α → γ → α be two binary operations. If the collection of all values obtainable by f, when the second argument varies, is contained in the collection obtainable by g, i.e. Range(a,c ↦ f c a) ⊆ Range(b,c ↦ g c b), then for every starting value a ∈ α, the range of foldl f a is contained in the range of foldl g a.
Русский
Пусть f: α → β → α и g: α → γ → α — две бинарные операции. Если множество значений, достигаемых функцией f при варьировании второго аргумента (для фиксированного первого аргумента a), вложено в множество значений, достигаемых функцией g, то для любого начала a ∈ α множество значений, достигаемых сверткой foldl f a, вложено в множество значений foldl g a.
LaTeX
$$$\\big(\\operatorname{Range}(a,c \\mapsto f\\,c\\,a) \\subseteq \\operatorname{Range}(b,c \\mapsto g\\,c\\,b)\\big) \\Rightarrow \\forall a:\\alpha, \\ \\operatorname{Range}(\\mathrm{foldl}\\ f\\ a) \\subseteq \\operatorname{Range}(\\mathrm{foldl}\\ g\\ a).$$$
Lean4
theorem foldl_range_subset_of_range_subset {f : α → β → α} {g : α → γ → α}
(hfg : (Set.range fun a c => f c a) ⊆ Set.range fun b c => g c b) (a : α) :
Set.range (foldl f a) ⊆ Set.range (foldl g a) :=
by
change
(Set.range fun l => _) ⊆
Set.range fun l =>
_
-- Porting note: have to write `(foldr_reverse)` instead of `foldr_reverse`.
simp_rw [← (foldr_reverse), Set.range_comp' _ reverse, reverse_involutive.bijective.surjective.range_eq,
Set.image_univ]
exact foldr_range_subset_of_range_subset hfg a
