Commit 2024-08-19 17:32 53c8ce8a

View on Github →

feat: Kleene's fixed point theorem (#13075) Add the fixed point theorem for (omega) complete partial orders and Kleene's fixed point theorem for complete lattices.

Estimated changes

Modified Mathlib/Order/FixedPoints.lean

added theorem fixedPoints.gfp_eq_sInf_iterate

added theorem fixedPoints.lfp_eq_sSup_iterate

Modified Mathlib/Order/OmegaCompletePartialOrder.lean

added def OmegaCompletePartialOrder.fixedPoints.iterateChain

added theorem OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_le_fixedPoint

added theorem OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_le_prefixedPoint

added theorem OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_mem_fixedPoint