Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-04 11:10 e24f7f7a

View on Github →

move(set_theory/ordinal/{arithmetic → fixed_points}): Move nfp (#13315) That way, it belong with the other functions about fixed points.

Estimated changes

deleted def ordinal.deriv
deleted theorem ordinal.deriv_eq_enum_fp
deleted theorem ordinal.deriv_is_normal
deleted theorem ordinal.deriv_limit
deleted theorem ordinal.deriv_mul_zero
deleted theorem ordinal.deriv_succ
deleted theorem ordinal.deriv_zero
deleted theorem ordinal.is_normal.le_nfp
deleted theorem ordinal.is_normal.nfp_fp
deleted theorem ordinal.iterate_le_nfp
deleted theorem ordinal.le_nfp_self
deleted theorem ordinal.lt_nfp
deleted def ordinal.nfp
deleted theorem ordinal.nfp_add_zero
deleted theorem ordinal.nfp_eq_self
deleted theorem ordinal.nfp_le
deleted theorem ordinal.nfp_le_iff
deleted theorem ordinal.nfp_mul_one
deleted theorem ordinal.nfp_mul_zero
deleted theorem ordinal.nfp_zero_mul
added def ordinal.deriv
added theorem ordinal.deriv_limit
added theorem ordinal.deriv_mul_zero
added theorem ordinal.deriv_succ
added theorem ordinal.deriv_zero
added theorem ordinal.fp_unbounded
added theorem ordinal.iterate_le_nfp
added theorem ordinal.le_nfp
modified theorem ordinal.le_nfp_bfamily
added theorem ordinal.le_nfp_family
added theorem ordinal.lt_nfp
added def ordinal.nfp
added theorem ordinal.nfp_add_zero
added theorem ordinal.nfp_eq_self
added theorem ordinal.nfp_id
added theorem ordinal.nfp_le
added theorem ordinal.nfp_le_fp
added theorem ordinal.nfp_le_iff
added theorem ordinal.nfp_monotone
added theorem ordinal.nfp_mul_one
added theorem ordinal.nfp_mul_zero
added theorem ordinal.nfp_zero_mul