Theorem not_injective_of_ordinal_of_small
Modification history
2025-08-22 21:50
Mathlib/SetTheory/Ordinal/Family.lean
chore: reprove `Ordinal.not_surjective_of_ordinal` without `Ordinal.lsub` (#28751) …
Deleted not_injective_of_ordinal_of_smallView on Github →