Commit 2023-02-26 15:22 c6b53304
View on Github →feat(set_theory/ordinal/fixed_point): add missing theorem (#18323)
We add apply_lt_nfp_bfamily matching apply_lt_nfp_family, and rename the existing theorem with that name to apply_lt_nfp_bfamily_iff, matching apply_lt_nfp_family_iff.