Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-16 18:58 9084a3c7

View on Github →

chore(order/fixed_point): add docstring for Knaster-Tarski theorem (#7589) clarify that the def provided constitutes the Knaster-Tarski theorem

Estimated changes

added theorem fixed_points.le_next
modified theorem fixed_points.next_eq
deleted theorem fixed_points.next_le
modified theorem fixed_points.prev_eq
modified theorem fixed_points.prev_le
modified theorem gfp_comp
deleted theorem gfp_eq
added theorem gfp_fixed_point
modified theorem gfp_gfp
deleted theorem gfp_induct
added theorem gfp_induction
modified theorem gfp_le
modified theorem le_gfp
modified theorem le_lfp
modified theorem lfp_comp
deleted theorem lfp_eq
added theorem lfp_fixed_point
deleted theorem lfp_induct
added theorem lfp_induction
modified theorem lfp_le
modified theorem lfp_lfp
modified theorem monotone_gfp
modified theorem monotone_lfp