Zulip Chat Archive

Stream: Is there code for X?

Topic: card_le_of


view this post on Zulip 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 :=
_

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (May 24 2020 at 15:35):

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

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (May 24 2020 at 16:46):

Preferably avoiding mentions of cardinal

view this post on Zulip 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

view this post on Zulip Bhavik Mehta (May 24 2020 at 19:58):

Yeah this

view this post on Zulip Kenny Lau (May 24 2020 at 20:09):

yes it failed


Last updated: May 17 2021 at 14:12 UTC