Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-04 15:09 fa520678

View on Github →

refactor(order/fixed_points): rewrite using bundled preorder_homs (#9497) This way fixed_points.complete_lattice can be an instance.

Estimated changes

modified theorem set.inj_on_empty
added theorem set.inj_on_singleton
added theorem set.inj_on_union
deleted theorem fixed_points.le_next
deleted def fixed_points.next
deleted theorem fixed_points.next_eq
deleted def fixed_points.prev
deleted theorem fixed_points.prev_eq
deleted theorem fixed_points.prev_le
deleted def gfp
deleted theorem gfp_comp
deleted theorem gfp_fixed_point
deleted theorem gfp_gfp
deleted theorem gfp_induction
deleted theorem gfp_le
deleted theorem le_gfp
deleted theorem le_lfp
deleted def lfp
deleted theorem lfp_comp
deleted theorem lfp_fixed_point
deleted theorem lfp_induction
deleted theorem lfp_le
deleted theorem lfp_lfp
deleted theorem monotone_gfp
deleted theorem monotone_lfp
added def preorder_hom.gfp
added theorem preorder_hom.gfp_gfp
added theorem preorder_hom.gfp_le
added theorem preorder_hom.le_gfp
added theorem preorder_hom.le_lfp
added def preorder_hom.lfp
added theorem preorder_hom.lfp_le
added theorem preorder_hom.lfp_lfp
added theorem preorder_hom.map_gfp
added theorem preorder_hom.map_lfp