Iterates of inflationary maps on the finsets of a finite type

A map f on the finsets of a finite type α that enlarges every finset, s ⊆ f s, can grow a finset only Fintype.card α times before it stops. This file records the resulting bound: the Fintype.card α-th iterate of f at any starting finset is a fixed point of f. It is the termination argument behind every closure computed by "repeat until nothing changes" on a finite carrier, stated once so that such computations can iterate a fixed number of times and remain executable.

Mathlib's Finset.image_iterate_stabilises_le_card is the analogous statement for the decreasing sequence of images of a finset under the iterates of a self-map of α; here the sequence is increasing and the map acts on finsets.

Main results

• Finset.isFixedPt_iterate_card: for f with s ⊆ f s for all s, the finset f^[Fintype.card α] s is a fixed point of f.

theorem Finset.isFixedPt_iterate_card {α : Type u_1} [Fintype α] {f : Finset α → Finset α} (hf : ∀ (s : Finset α), s ⊆ f s) (s : Finset α) : Function.IsFixedPt f (f^[Fintype.card α] s)

An inflationary self-map of the finsets of a finite type reaches a fixed point after Fintype.card α iterations, whatever the starting finset: the iterates form an increasing chain of finsets, and such a chain can grow strictly at most Fintype.card α times.