Theorem nonempty_fun

Modification history

2026-02-13 18:17
Mathlib/Logic/IsEmpty.lean
chore(Logic/IsEmpty): split file into `Defs` and `Basic` (#35137) …
Modified nonempty_funView on Github →
2024-01-12 06:00
Mathlib/Logic/IsEmpty.lean
feat(Cardinal): `#(α ≃ β)` and `#(α ↪ β)` in the infinite case (#9646) …
Added nonempty_funView on Github →