Commit 2025-02-17 21:24 47f9c57c

View on Github →

chore(SetTheory/Ordinal/FixedPoint): small clean-up (#21970) This PR does the following:

  • fix the names lt_nfpFamily → lt_nfpFamily_iff and lt_nfp → lt_nfp_iff, matching lt_iSup_iff.
  • remove some redundant arguments

Estimated changes

modified theorem Ordinal.IsNormal.deriv_fp
modified theorem Ordinal.IsNormal.nfp_fp
modified theorem Ordinal.deriv_id_of_nfp_id
deleted theorem Ordinal.lt_nfp
deleted theorem Ordinal.lt_nfpFamily
added theorem Ordinal.lt_nfp_iff
modified theorem Ordinal.nfp_eq_self
modified theorem Ordinal.nfp_le_fp