card_le_of

Stream: Is there code for X?

[Kenny Lau]

import set_theory.cardinal

universe u

theorem card_le_of {α : Type u} {n : ℕ} (H : ∀ s : finset α, s.card ≤ n) :
  cardinal.mk α ≤ n :=
_

[Kenny Lau]

this says that if every finite subset of A has size less than or equal to a given natural number n, then the cardinality of A is less than or equal to n

[Kenny Lau]

import set_theory.cardinal

universe u

theorem card_le_of {α : Type u} {n : ℕ} (H : ∀ s : finset α, s.card ≤ n) :
  cardinal.mk α ≤ n :=
begin
  refine le_of_not_lt (λ hn, _),
  have := cardinal.succ_le.2 hn,
  rw [← cardinal.nat_succ, ← cardinal.lift_mk_fin n.succ] at this,
  cases this,
  refine not_lt_of_le (H $ finset.univ.map this) _,
  rw [finset.card_map, ← fintype.card, fintype.card_ulift, fintype.card_fin],
  exact n.lt_succ_self
end

[Kenny Lau]

I feel like there should be a shorter proof though....

[Bhavik Mehta]

I think there ought to be something in the library letting us show α is a fintype under your hypotheses

[Bhavik Mehta]

Preferably avoiding mentions of cardinal

[Kenny Lau]

import data.fintype.card

universe u

theorem card_le_of {α : Type u} {n : ℕ} (H : ∀ s : finset α, s.card ≤ n) : fintype α :=
by library_search -- failed

[Bhavik Mehta]

Yeah this

[Kenny Lau]

yes it failed