Commit 2024-12-23 21:59 64248df7

feat(Order): the transfinite iteration of a map (#19935) Given φ : I → I where [SupSet I], we define the jth transfinite iteration of φ for any j : J, with J a well-ordered type: this is transfiniteIterate φ j : I → I. If i₀ : I, then transfiniteIterate φ ⊥ i₀ = i₀; if j is a non maximal element, than transfiniteIterate φ (Order.succ j) i₀ = φ (transfiniteIterate φ j i₀); and if j is a limit element, transfiniteIterate φ j i₀ is the supremum of the transfiniteIterate φ l i₀ for l < j. (Hopefully, this will be used in order to show Grothendieck abelian categories have enough injectives.)