Theorem Function.exists_surjective_iff

Modification history

2024-04-19 20:51

Mathlib/Logic/Embedding/Basic.lean

chore(Logic): reduce use of autoImplicit (#12135) …

Modified Function.exists_surjective_iff View on Github →

2024-01-12 06:00

Mathlib/Logic/Embedding/Basic.lean

feat(Cardinal): `#(α ≃ β)` and `#(α ↪ β)` in the infinite case (#9646) …

Added Function.exists_surjective_iff View on Github →