Zulip Chat Archive

Stream: new members

Topic: complement of finset in infinite set


view this post on Zulip Iocta (Aug 19 2020 at 00:19):

import data.set.basic
import data.set.finite
import data.nat.basic

example (s: set  ) (h: set.finite s) : set.infinite s := _

Is this in mathlib?

view this post on Zulip Iocta (Aug 19 2020 at 00:22):

I started working on it but it seemed to need a bunch of lemmas I couldn't find

view this post on Zulip Adam Topaz (Aug 19 2020 at 00:33):

I wonder if there is a straightforward proof with cardinality?

view this post on Zulip Alex J. Best (Aug 19 2020 at 00:34):

mk_compl_of_omega_le seems useful?

view this post on Zulip Adam Topaz (Aug 19 2020 at 00:35):

Presumably there is also a lemma stating that a set of cardinality omega is infinite?

view this post on Zulip Alex J. Best (Aug 19 2020 at 00:44):

open cardinal
example (s: set  ) (h: set.finite s) : set.infinite s :=
begin
  rw [ set.infinite_coe_iff, infinite_iff, mk_compl_of_omega_le s _ _],
  all_goals {rw mk_nat,},
  exact lt_omega_iff_finite.mpr h,
end

view this post on Zulip Alex J. Best (Aug 19 2020 at 00:45):

Probably this can be made into a 2-liner xD

view this post on Zulip Kyle Miller (Aug 19 2020 at 00:50):

I don't know how to navigate the finset/fintype API well enough to finish this quickly, but another approach is to first transform it by something like

example (s: set ) (h: set.finite s) : set.infinite s :=
begin
  intro h',
  tactic.unfreeze_local_instances,
  cases h, cases h',
  dsimp [compl, boolean_algebra.compl, set.compl] at h',
  sorry
end

so then the context is

s : set ,
h : fintype s,
h' : fintype {a :  | a  s}
 false

If you let m and m' be the maximal elements in the two sets, then 1 + max m m' is in neither set, contradicting the fact that the sets are complements.

view this post on Zulip Kyle Miller (Aug 19 2020 at 00:51):

(I know the question is "is this in mathlib," which this certainly doesn't help you in answering.)

view this post on Zulip Mario Carneiro (Aug 19 2020 at 01:00):

I would suggest:

example (s: set ) (h: set.finite s) : set.infinite s :=
begin
  intro h',
  apply set.infinite_univ_iff.2 nat.infinite,
  simpa using h.union h',
end

view this post on Zulip Kenny Lau (Aug 19 2020 at 06:40):

example (s : set ) (hs : set.finite s) : set.infinite s :=
λ hsc, @set.infinite_univ  _ $ set.union_compl_self s  hs.union hsc

Last updated: May 15 2021 at 00:39 UTC