## Stream: Is there code for X?

### Topic: card_le_of

#### Kenny Lau (May 24 2020 at 15:19):

import set_theory.cardinal

universe u

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


#### Kenny Lau (May 24 2020 at 15:21):

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 (May 24 2020 at 15:35):

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 (May 24 2020 at 15:35):

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

#### Bhavik Mehta (May 24 2020 at 16:44):

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

#### Bhavik Mehta (May 24 2020 at 16:46):

Preferably avoiding mentions of cardinal

#### Kenny Lau (May 24 2020 at 19:46):

import data.fintype.card

universe u

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


Yeah this

#### Kenny Lau (May 24 2020 at 20:09):

yes it failed

Last updated: May 17 2021 at 14:12 UTC