feat(set_theory/cardinal): finite lower bound on cardinality

Author: digama0

data/fintype.lean

@@ -315,6 +315,9 @@ instance finset.subtype.fintype (s : finset α) : fintype {x // x ∈ s} :=
 instance finset_coe.fintype (s : finset α) : fintype (↑s : set α) :=
 finset.subtype.fintype s
 
+@[simp] lemma fintype.card_coe (s : finset α) :
+  fintype.card (↑s : set α) = s.card := card_attach
+
 instance plift.fintype (p : Prop) [decidable p] : fintype (plift p) :=
 ⟨if h : p then finset.singleton ⟨h⟩ else ∅, λ ⟨h⟩, by simp [h]⟩
 

data/set/finite.lean

@@ -55,6 +55,10 @@ noncomputable def finite.to_finset {s : set α} (h : finite s) : finset α :=
 @[simp] theorem finite.mem_to_finset {s : set α} {h : finite s} {a : α} : a ∈ h.to_finset ↔ a ∈ s :=
 @mem_to_finset _ _ (finite.fintype h) _
 
+theorem finite.exists_finset {s : set α} : finite s →
+  ∃ s' : finset α, ∀ a : α, a ∈ s' ↔ a ∈ s
+| ⟨h⟩ := by exactI ⟨to_finset s, λ _, mem_to_finset⟩
+
 theorem finite_mem_finset (s : finset α) : finite {a | a ∈ s} :=
 ⟨fintype_of_finset s (λ _, iff.rfl)⟩
 

set_theory/cardinal.lean

@@ -525,6 +525,14 @@ theorem fintype_card (α : Type u) [fintype α] : mk α = fintype.card α :=
 by rw [← lift_mk_fin.{u}, ← lift_id (mk α), lift_mk_eq.{u 0 u}];
    exact fintype.card_eq.1 (by simp)
 
+theorem card_le_of_finset {α} (s : finset α) :
+  (s.card : cardinal) ≤ cardinal.mk α :=
+begin
+  rw (_ : (s.card : cardinal) = cardinal.mk (↑s : set α)),
+  { exact ⟨function.embedding.subtype _⟩ },
+  rw [cardinal.fintype_card, fintype.card_coe]
+end
+
 @[simp] theorem nat_cast_pow {m n : ℕ} : (↑(pow m n) : cardinal) = m ^ n :=
 by induction n; simp [nat.pow_succ, -_root_.add_comm, power_add, *]