Finite folds

Small order-theoretic facts about folds indexed by Fin.

theorem Algebraic.Fin.le_foldl_max {α : Type u_1} {n : ℕ} [LinearOrder α] (values : Fin n → α) (initial : α) (i : Fin n) : values i ≤ Fin.foldl n (fun (result : α) (j : Fin n) => max result (values j)) initial

Every folded value is at most the maximum accumulated by Fin.foldl.

theorem Algebraic.Fin.foldl_max_le {α : Type u_1} {n : ℕ} [LinearOrder α] (values : Fin n → α) (initial bound : α) (initial_le : initial ≤ bound) (values_le : ∀ (i : Fin n), values i ≤ bound) : Fin.foldl n (fun (result : α) (i : Fin n) => max result (values i)) initial ≤ bound

A finite maximum is bounded above when its initial value and every folded value are bounded above.