Commit 2024-11-23 05:51 a7f12adc

View on Github →

chore(Order/FixedPoints): remove adaptation notes for OrderHom regarding lean4 issue #1910 (#19380) this PR removes 3 porting notes regarding lean4 issue leanprover/lean4#1910, and makes adaptations to mathlib to make use of the newly working notation. Concretely, that means that OrderHom.lfp f now is written f.lfp, and similar for OrderHom.dual and OrderHom.gfp. there might still be some dual x application left inside code with open OrderHom, but those are hard to filter for with grep, as there are many declarations named dual in different namespaces.

Estimated changes

modified theorem OrderHom.gfp_const_inf_le
modified theorem OrderHom.gfp_gfp
modified theorem OrderHom.gfp_induction
modified theorem OrderHom.gfp_le
modified theorem OrderHom.gfp_le_map
modified theorem OrderHom.isFixedPt_gfp
modified theorem OrderHom.isFixedPt_lfp
modified theorem OrderHom.isGreatest_gfp
modified theorem OrderHom.isGreatest_gfp_le
modified theorem OrderHom.isLeast_lfp
modified theorem OrderHom.isLeast_lfp_le
modified theorem OrderHom.le_gfp
modified theorem OrderHom.le_lfp
modified theorem OrderHom.lfp_induction
modified theorem OrderHom.lfp_le
modified theorem OrderHom.lfp_le_fixed
modified theorem OrderHom.lfp_le_map
modified theorem OrderHom.lfp_lfp
modified theorem OrderHom.map_gfp
modified theorem OrderHom.map_gfp_comp
modified theorem OrderHom.map_le_gfp
modified theorem OrderHom.map_le_lfp
modified theorem OrderHom.map_lfp
modified theorem OrderHom.map_lfp_comp
modified theorem OrderHom.dual_id
modified theorem BoundedOrderHom.dual_id
modified theorem Interval.dual_map