Commit 2022-02-10 09:27 0aa0bc8f

View on Github →

feat(set_theory/ordinal_arithmetic): The derivative of addition (#11270) We prove that the derivative of (+) a evaluated at b is given by a * ω + b.

Estimated changes

Modified src/set_theory/ordinal_arithmetic.lean

added theorem ordinal.add_eq_right_iff_mul_omega_le

added theorem ordinal.add_le_right_iff_mul_omega_le

added theorem ordinal.deriv_add_eq_mul_omega_add

modified def ordinal.family_of_bfamily

modified theorem ordinal.family_of_bfamily_enum

added theorem ordinal.is_normal.apply_eq_self_iff_deriv

modified theorem ordinal.is_normal.deriv_fp

deleted theorem ordinal.is_normal.fp_iff_deriv'

deleted theorem ordinal.is_normal.fp_iff_deriv

added theorem ordinal.is_normal.le_iff_deriv

added theorem ordinal.is_normal.le_iff_eq

modified theorem ordinal.is_normal.le_nfp

modified theorem ordinal.is_normal.nfp_fp

deleted theorem ordinal.is_normal.nfp_le

modified theorem ordinal.is_normal.nfp_le_fp

added theorem ordinal.mul_one_add

added theorem ordinal.nfp_add_eq_mul_omega

added theorem ordinal.nfp_add_zero

modified theorem ordinal.nfp_eq_self

modified theorem ordinal.sup_add_nat

modified theorem ordinal.sup_mul_nat

modified theorem ordinal.sup_nat_cast