From 38904ac8c3a469b455eb2501a395c0901b251ef1 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 30 Jun 2020 04:15:21 +0000 Subject: [PATCH] feat(data/fintype/basic): card_eq_zero_equiv_equiv_pempty (#3238) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds a constructive equivalence `α ≃ pempty.{v+1}` given `fintype.card α = 0`, which I think wasn't available previously. I would have stated this as an `iff`, but as the right hand side is data is an `equiv` itself. Co-authored-by: Scott Morrison --- src/data/fintype/basic.lean | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/src/data/fintype/basic.lean b/src/data/fintype/basic.lean index f0a12d04be679..00f2ec86bfa65 100644 --- a/src/data/fintype/basic.lean +++ b/src/data/fintype/basic.lean @@ -426,6 +426,19 @@ lemma fintype.card_eq_zero_iff [fintype α] : fintype.card α = 0 ↔ (α → fa λ h, have e : α ≃ empty := ⟨λ a, (h a).elim, λ a, a.elim, λ a, (h a).elim, λ a, a.elim⟩, by simp [fintype.card_congr e]⟩ +/-- A `fintype` with cardinality zero is (constructively) equivalent to `pempty`. -/ +def fintype.card_eq_zero_equiv_equiv_pempty {α : Type v} [fintype α] : + fintype.card α = 0 ≃ (α ≃ pempty.{v+1}) := +{ to_fun := λ h, + { to_fun := λ a, false.elim (fintype.card_eq_zero_iff.1 h a), + inv_fun := λ a, pempty.elim a, + left_inv := λ a, false.elim (fintype.card_eq_zero_iff.1 h a), + right_inv := λ a, pempty.elim a, }, + inv_fun := λ e, + by { simp only [←fintype.of_equiv_card e], convert fintype.card_pempty, }, + left_inv := λ h, rfl, + right_inv := λ e, by { ext x, cases e x, } } + lemma fintype.card_pos_iff [fintype α] : 0 < fintype.card α ↔ nonempty α := ⟨λ h, classical.by_contradiction (λ h₁, have fintype.card α = 0 := fintype.card_eq_zero_iff.2 (λ a, h₁ ⟨a⟩),