Least fixed points on finite powersets

A monotone map on subsets of a finite type reaches its least fixed point by iterating from the empty set at most the cardinality of the underlying type times. This is the number of elements, not the cardinality of the powerset. No inflationarity assumption is needed: the iteration from the empty set is increasing by monotonicity.

Main results

• OrderHom.iterate_bot_le_lfp: every iterate from the bottom lies below the least fixed point.
• OrderHom.iterate_card_bot_eq_lfp: on Set α, the iterate at Fintype.card α is the least fixed point, including when α is empty.
• OrderHom.iterate_bot_eq_lfp_of_card_le: every subsequent iterate has the same value.

theorem OrderHom.iterate_bot_le_lfp {β : Type u_2} [CompleteLattice β] (f : β →o β) (n : ℕ) : (⇑f)^[n] ⊥ ≤ lfp f

Every finite iterate from the bottom lies below the least fixed point.

theorem OrderHom.iterate_card_bot_eq_lfp {α : Type u_1} [Fintype α] (f : Set α →o Set α) : (⇑f)^[Fintype.card α] ⊥ = lfp f

A monotone map on a finite powerset reaches its least fixed point from the empty set after at most the cardinality of the underlying type many iterations.

theorem OrderHom.iterate_bot_eq_lfp_of_card_le {α : Type u_1} [Fintype α] (f : Set α →o Set α) {n : ℕ} (hn : Fintype.card α ≤ n) : (⇑f)^[n] ⊥ = lfp f

Every iteration at or beyond the finite powerset bound equals the least fixed point.