Zulip Chat Archive

Stream: new members

Topic: noob question about cardinal


view this post on Zulip Kenny Lau (Sep 13 2018 at 09:04):

import set_theory.cardinal

example (α : Type*) (S T : set α)
  (HS : set.finite S) (HT : set.finite T)
  (H : finset.card (set.finite.to_finset HS)  finset.card (set.finite.to_finset HT)) :
  cardinal.mk S  cardinal.mk T :=
sorry

view this post on Zulip Chris Hughes (Sep 13 2018 at 09:41):

open cardinal

example (α : Type*) (S T : set α)
  (HS : set.finite S) (HT : set.finite T)
  (H : finset.card (set.finite.to_finset HS)  finset.card (set.finite.to_finset HT)) :
  cardinal.mk S  cardinal.mk T :=
begin
  haveI := classical.choice HS,
  haveI := classical.choice HT,
  rwa [fintype_card S, fintype_card T, nat_cast_le,
    set.card_fintype_of_finset' (set.finite.to_finset HS),
    set.card_fintype_of_finset' (set.finite.to_finset HT)];
  simp
end

view this post on Zulip Kenny Lau (Sep 13 2018 at 09:43):

import set_theory.cardinal

example (α : Type*) (S T : set α)
  (HS : set.finite S) (HT : set.finite T)
  (H : finset.card (set.finite.to_finset HS)  finset.card (set.finite.to_finset HT)) :
  cardinal.mk S  cardinal.mk T :=
begin
  tactic.unfreeze_local_instances,
  cases HS, cases HT,
  rw [cardinal.fintype_card, cardinal.fintype_card, cardinal.nat_cast_le],
  rw [ fintype.card_coe,  fintype.card_coe] at H,
  convert H;
  { ext z, rw [finset.mem_coe, set.finite.mem_to_finset] }
end

view this post on Zulip Kenny Lau (Sep 13 2018 at 09:44):

anyway why do we need so many lines


Last updated: May 12 2021 at 23:13 UTC