Commit 2021-05-18 04:50 3694945d

feat(logic/is_empty): Add is_empty typeclass (#7606)

• Refactor some equivalences that use empty or pempty.
• Replace α → false with is_empty α in various places (but not everywhere, we can do that in follow-up PRs).
• infinite is proven equivalent to is_empty (fintype α). The old not_fintype is renamed to fintype.false (to allow projection notation), and there are two useful variants infinite.false and not_fintype added with different arguments explicit.
• add instance unique true.
• Changed the type of fin_one_equiv from fin 1 ≃ punit to fin 1 ≃ unit (it was used only once, where the former formulation required giving an explicit universe level).
• renamings: equiv.subsingleton_iff -> equiv.subsingleton_congr finprod_of_empty -> finprod_of_is_empty