Zulip Chat Archive

Stream: general

Topic: card_nonempty


Johan Commelin (Sep 08 2018 at 18:44):

Is there some easy way to tackle this goal:

n : Type u,
_inst_1 : fintype n,
h : nonempty n
 0 < fintype.card n

Kenny Lau (Sep 08 2018 at 18:48):

import data.fintype

universe u
variables (n : Type u) [fintype n]
example (h : nonempty n) : 0 < fintype.card n :=
begin
  by_contra H,
  rw [not_lt, nat.le_zero_iff, fintype.card_eq_zero_iff] at H,
  exact h.rec_on H
end

Johan Commelin (Sep 08 2018 at 18:50):

I guess this could be a simp lemma in mathlib?

Johan Commelin (Sep 08 2018 at 18:50):

Ooh, and thanks!

Kenny Lau (Sep 08 2018 at 18:54):

import set_theory.cardinal

universe u
variables (n : Type u)
example (h : nonempty n) : 0 < cardinal.mk n :=
by rwa [cardinal.pos_iff_ne_zero, cardinal.ne_zero_iff_nonempty]

Kenny Lau (Sep 08 2018 at 18:54):

I think Mario likes cardinal.mk more than fintype.card

Chris Hughes (Sep 08 2018 at 18:59):

It is in mathlib. fintype.card_pos_iff I believe.

Johan Commelin (Sep 08 2018 at 19:02):

Aaah, thanks! (Sorry, Kenny)


Last updated: Dec 20 2023 at 11:08 UTC