mathlib
c6b53304
- feat(set_theory/ordinal/fixed_point): add missing theorem (#18323)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
2 years ago
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`.
Author
vihdzp
Parents
146a2eed
Loading