Commit 2021-09-30 08:02 f6d2434f
View on Github →feat(set_theory/cardinal_ordinal): there is no injective function from ordinals to types in the same universe (#9452) Contributed by @rwbarton at https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Transfinite.20recursion/near/253614140