English
If the sets of outputs obtainable by the two-argument functions a ↦ f c a and b ↦ g c b are equal, then for every starting value a ∈ α, the ranges of the left-folds are equal: Set.range (foldl f a) = Set.range (foldl g a).
Русский
Если множества выходов функций f и g одинаковы, то для каждого a ∈ α диапазоны получаемых значений foldl f a и foldl g a совпадают.
LaTeX
$$$\\operatorname{Set.range}(a,c \\mapsto f c a) = \\operatorname{Set.range}(b,c \\mapsto g c b) \\Rightarrow \\forall a:\\alpha, \\ \\operatorname{Set.range}(\\mathrm{foldl}\\ f\\ a) = \\operatorname{Set.range}(\\mathrm{foldl}\\ g\\ a).$$$
Lean4
theorem foldl_range_eq_of_range_eq {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) :=
(foldl_range_subset_of_range_subset hfg.le a).antisymm (foldl_range_subset_of_range_subset hfg.ge a)
