Zulip Chat Archive

Stream: new members

Topic: Working with sets of finite cardinality


view this post on Zulip Patrick Lutz (Jul 08 2020 at 21:33):

I am having trouble figuring out how to do something very basic when working with finite sets. The following is an illustration of the kind of thing I can't figure out how to do:

import data.fintype.basic
example (X : Type) [fintype X] (a b c : X) (h : fintype.card X = 2)
    (h1 : a  b) (h2 : a  c) (h3 : b  c) : false := sorry

What's the best way to prove this kind of thing?

view this post on Zulip Mario Carneiro (Jul 08 2020 at 21:36):

I would try to prove that [a,b,c] induces a finset of size 3

view this post on Zulip Mario Carneiro (Jul 08 2020 at 21:40):

import data.fintype.basic
example (X : Type) [fintype X] (a b c : X) (h : fintype.card X = 2)
    (h1 : a  b) (h2 : a  c) (h3 : b  c) : false :=
begin
  let S : finset X := [a,b,c], by simp *⟩,
  have : 3  _ := finset.card_le_of_subset (finset.subset_univ S),
  rw [finset.card_univ, h] at this,
  exact absurd this dec_trivial,
end

view this post on Zulip Patrick Lutz (Jul 08 2020 at 22:42):

Nice, thanks. That works


Last updated: May 15 2021 at 00:39 UTC