Commit 2022-12-23 15:45 49c9c7c0

View on Github →

feat: port Order.FixedPoints (#1174)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/FixedPoints.lean

added def OrderHom.gfp

added theorem OrderHom.gfp_const_inf_le

added theorem OrderHom.gfp_gfp

added theorem OrderHom.gfp_induction

added theorem OrderHom.gfp_le

added theorem OrderHom.gfp_le_map

added theorem OrderHom.isFixedPt_gfp

added theorem OrderHom.isFixedPt_lfp

added theorem OrderHom.isGreatest_gfp

added theorem OrderHom.isGreatest_gfp_le

added theorem OrderHom.isLeast_lfp

added theorem OrderHom.isLeast_lfp_le

added theorem OrderHom.le_gfp

added theorem OrderHom.le_lfp

added theorem OrderHom.le_map_sup_fixedPoints

added theorem OrderHom.le_map_supₛ_subset_fixedPoints

added theorem OrderHom.le_nextFixed

added theorem OrderHom.le_prevFixed

added theorem OrderHom.le_prevFixed_iff

added def OrderHom.lfp

added theorem OrderHom.lfp_induction

added theorem OrderHom.lfp_le

added theorem OrderHom.lfp_le_fixed

added theorem OrderHom.lfp_le_map

added theorem OrderHom.lfp_lfp

added theorem OrderHom.map_gfp

added theorem OrderHom.map_gfp_comp

added theorem OrderHom.map_inf_fixedPoints_le

added theorem OrderHom.map_infₛ_subset_fixedPoints_le

added theorem OrderHom.map_le_gfp

added theorem OrderHom.map_le_lfp

added theorem OrderHom.map_lfp

added theorem OrderHom.map_lfp_comp

added def OrderHom.nextFixed

added theorem OrderHom.nextFixed_le

added theorem OrderHom.nextFixed_le_iff

added def OrderHom.prevFixed

added theorem OrderHom.prevFixed_le