Commit 2023-02-21 15:14 628f140f

View on Github →

feat: port SetTheory.Ordinal.FixedPoint (#2416)

Estimated changes

Modified Mathlib.lean

Created Mathlib/SetTheory/Ordinal/FixedPoint.lean

added theorem Ordinal.IsNormal.apply_le_nfp

added theorem Ordinal.IsNormal.apply_lt_nfp

added theorem Ordinal.IsNormal.deriv_fp

added theorem Ordinal.IsNormal.fp_iff_deriv

added theorem Ordinal.IsNormal.le_iff_deriv

added theorem Ordinal.IsNormal.nfp_fp

added theorem Ordinal.IsNormal.nfp_le_apply

added theorem Ordinal.add_eq_right_iff_mul_omega_le

added theorem Ordinal.add_le_right_iff_mul_omega_le

added theorem Ordinal.apply_le_nfpBFamily

added theorem Ordinal.apply_le_nfpFamily

added theorem Ordinal.apply_lt_nfpBFamily

added theorem Ordinal.apply_lt_nfpFamily

added theorem Ordinal.apply_lt_nfpFamily_iff

added def Ordinal.deriv

added def Ordinal.derivBFamily

added theorem Ordinal.derivBFamily_eq_derivFamily

added theorem Ordinal.derivBFamily_eq_enumOrd

added theorem Ordinal.derivBFamily_fp

added theorem Ordinal.derivBFamily_isNormal

added def Ordinal.derivFamily

added theorem Ordinal.derivFamily_eq_enumOrd

added theorem Ordinal.derivFamily_fp

added theorem Ordinal.derivFamily_isNormal

added theorem Ordinal.derivFamily_limit

added theorem Ordinal.derivFamily_succ

added theorem Ordinal.derivFamily_zero

added theorem Ordinal.deriv_add_eq_mul_omega_add

added theorem Ordinal.deriv_eq_derivFamily

added theorem Ordinal.deriv_eq_enumOrd

added theorem Ordinal.deriv_eq_id_of_nfp_eq_id

added theorem Ordinal.deriv_id_of_nfp_id

added theorem Ordinal.deriv_isNormal

added theorem Ordinal.deriv_limit

added theorem Ordinal.deriv_mul_eq_opow_omega_mul

added theorem Ordinal.deriv_mul_zero

added theorem Ordinal.deriv_succ

added theorem Ordinal.deriv_zero

added theorem Ordinal.eq_zero_or_opow_omega_le_of_mul_eq_right

added theorem Ordinal.foldr_le_nfpBFamily

added theorem Ordinal.foldr_le_nfpFamily

added theorem Ordinal.fp_bfamily_unbounded

added theorem Ordinal.fp_family_unbounded

added theorem Ordinal.fp_iff_derivBFamily

added theorem Ordinal.fp_iff_derivFamily

added theorem Ordinal.fp_unbounded

added theorem Ordinal.iterate_le_nfp

added theorem Ordinal.le_iff_derivBFamily

added theorem Ordinal.le_iff_derivFamily

added theorem Ordinal.le_nfp

added theorem Ordinal.le_nfpBFamily

added theorem Ordinal.le_nfpFamily

added theorem Ordinal.lt_nfp

added theorem Ordinal.lt_nfpBFamily

added theorem Ordinal.lt_nfpFamily

added theorem Ordinal.mul_eq_right_iff_opow_omega_dvd

added theorem Ordinal.mul_le_right_iff_opow_omega_dvd

added def Ordinal.nfp

added def Ordinal.nfpBFamily

added theorem Ordinal.nfpBFamily_eq_nfpFamily

added theorem Ordinal.nfpBFamily_eq_self

added theorem Ordinal.nfpBFamily_fp

added theorem Ordinal.nfpBFamily_le

added theorem Ordinal.nfpBFamily_le_apply

added theorem Ordinal.nfpBFamily_le_fp

added theorem Ordinal.nfpBFamily_le_iff

added theorem Ordinal.nfpBFamily_monotone

added def Ordinal.nfpFamily

added theorem Ordinal.nfpFamily_eq_self

added theorem Ordinal.nfpFamily_eq_sup

added theorem Ordinal.nfpFamily_fp

added theorem Ordinal.nfpFamily_le

added theorem Ordinal.nfpFamily_le_apply

added theorem Ordinal.nfpFamily_le_fp

added theorem Ordinal.nfpFamily_le_iff

added theorem Ordinal.nfpFamily_monotone

added theorem Ordinal.nfp_add_eq_mul_omega

added theorem Ordinal.nfp_add_zero

added theorem Ordinal.nfp_eq_nfpFamily

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_eq_opow_omega

added theorem Ordinal.nfp_mul_one

added theorem Ordinal.nfp_mul_opow_omega_add

added theorem Ordinal.nfp_mul_zero

added theorem Ordinal.nfp_zero_mul

added theorem Ordinal.sup_iterate_eq_nfp