ω-suprema in complete lattices

Every complete lattice is an ω-complete partial order (through ChainCompletePartialOrder), and there the ω-supremum of a chain is its indexed supremum; on a product of complete lattices the same holds for the product instance. Kleene's fixed-point theorem then takes a supremum form that is independent of which of the two instances a continuity proof was carried out in (OrderHom.lfp_eq_iSup_iterate). [UPSTREAM] candidate for Mathlib/Order/OmegaCompletePartialOrder.lean and Mathlib/Order/FixedPoints.lean.

theorem CompleteLattice.ωSup_eq_iSup {L : Type u_1} [CompleteLattice L] (c : OmegaCompletePartialOrder.Chain L) : OmegaCompletePartialOrder.ωSup c = ⨆ (n : ℕ), c n

On a complete lattice, the ω-supremum of a chain is its indexed supremum.

theorem Pi.ωSup_eq_iSup {ι : Type u_1} {L : ι → Type u_2} [(i : ι) → CompleteLattice (L i)] (c : OmegaCompletePartialOrder.Chain ((i : ι) → L i)) : OmegaCompletePartialOrder.ωSup c = ⨆ (n : ℕ), c n

On a product of complete lattices, the ω-supremum of a chain is its indexed supremum.

theorem OrderHom.lfp_eq_iSup_iterate {L : Type u_1} [CompleteLattice L] (f : L →o L) (hf : ∀ (c : OmegaCompletePartialOrder.Chain L), f (⨆ (n : ℕ), c n) = ⨆ (n : ℕ), f (c n)) : lfp f = ⨆ (n : ℕ), (⇑f)^[n] ⊥

Kleene's fixed-point theorem in supremum form: a monotone map on a complete lattice that commutes with suprema of monotone sequences has the supremum of its iterates as least fixed point.