From 01fa7f5261740a676cb3ccccd9f3acb7a71105d3 Mon Sep 17 00:00:00 2001 From: tb65536 Date: Tue, 18 Jan 2022 07:45:51 +0000 Subject: [PATCH] feat(data/fintype/basic): `one_lt_card_iff` and `two_lt_card_iff` (#11524) This PR adds `one_lt_card_iff` and `two_lt_card_iff`. --- src/data/fintype/basic.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/data/fintype/basic.lean b/src/data/fintype/basic.lean index 5ad245acec039..d432836d72114 100644 --- a/src/data/fintype/basic.lean +++ b/src/data/fintype/basic.lean @@ -1023,6 +1023,12 @@ fintype.card_eq_one_iff.2 ⟨i,h⟩ lemma one_lt_card [h : nontrivial α] : 1 < fintype.card α := fintype.one_lt_card_iff_nontrivial.mpr h +lemma one_lt_card_iff : 1 < card α ↔ ∃ a b : α, a ≠ b := +one_lt_card_iff_nontrivial.trans nontrivial_iff + +lemma two_lt_card_iff : 2 < card α ↔ ∃ a b c : α, a ≠ b ∧ a ≠ c ∧ b ≠ c := +by simp_rw [←finset.card_univ, two_lt_card_iff, mem_univ, true_and] + lemma injective_iff_surjective {f : α → α} : injective f ↔ surjective f := by haveI := classical.prop_decidable; exact have ∀ {f : α → α}, injective f → surjective f,