Theorem Cardinal.mk_embedding_le_arrow

Modification history

2024-01-17 23:23
Mathlib/SetTheory/Cardinal/Ordinal.lean
chore(*): rename `FunLike` to `DFunLike` (#9785) …
Modified Cardinal.mk_embedding_le_arrowView on Github →
2024-01-12 06:00
Mathlib/SetTheory/Cardinal/Ordinal.lean
feat(Cardinal): `#(α ≃ β)` and `#(α ↪ β)` in the infinite case (#9646) …
Added Cardinal.mk_embedding_le_arrowView on Github →