Zulip Chat Archive

Stream: general

Topic: infinite sets


view this post on Zulip Kenny Lau (May 27 2019 at 16:08):

We know a lot of things about set.finite, but what do we know when the set is not finite?

view this post on Zulip Kenny Lau (May 27 2019 at 16:10):

for example:

theorem set.of_not_finite {s : set α} (hfs : ¬s.finite) :
   f :   α, function.injective f   n, f n  s :=
sorry

view this post on Zulip Mario Carneiro (May 27 2019 at 16:13):

that's equivalent to a cardinal theorem

view this post on Zulip Kenny Lau (May 27 2019 at 16:14):

how many lines would I need?

view this post on Zulip Kenny Lau (May 27 2019 at 16:34):

theorem set.of_not_finite {s : set α} (hfs : ¬s.finite) :
   f :   α, function.injective f   n, f n  s :=
begin
  have :  t : finset α,  x  s, x  t,
  { intros t, by_contradiction h, simp only [not_exists, not_not] at h,
    exact hfs (set.finite_subset (finset.finite_to_set t) h) },
  choose f hf1 hf2,
  refine nat.strong_rec' (λ n ih, f $ (finset.range n).attach.image $ λ x, _), _, _⟩,
  { exact ih x.1 (finset.mem_range.1 x.2) },
  { intros m n h, apply linarith.eq_of_not_lt_of_not_gt,
    { intros hmn, conv_rhs at h { rw nat.strong_rec' },
      apply hf2, rw [ h, finset.mem_image], use [m, finset.mem_range.2 hmn, finset.mem_attach _ _] },
    { intros hnm, conv_lhs at h { rw nat.strong_rec' },
      apply hf2, rw [h, finset.mem_image], use [n, finset.mem_range.2 hnm, finset.mem_attach _ _] } },
  { intros n, rw nat.strong_rec', exact hf1 _ }
end

view this post on Zulip Kenny Lau (May 27 2019 at 16:34):

14 lines without cardinal

view this post on Zulip Mario Carneiro (May 27 2019 at 16:37):

theorem set.of_not_finite {α} {s : set α} (hfs : ¬s.finite) :
   f :   α, function.injective f   n, f n  s :=
begin
  cases le_of_not_lt (mt cardinal.lt_omega_iff_finite.1 hfs) with f,
  replace f := equiv.ulift.symm.to_embedding.trans f,
  let g := f.trans (function.embedding.subtype s),
  exact g, g.2, λ x, (f x).2
end

view this post on Zulip Mario Carneiro (May 27 2019 at 16:38):

the proof is morally done after line 2 (you have ℕ ↪ ↥s) and the rest is making it fit your statement

view this post on Zulip Mario Carneiro (May 27 2019 at 16:39):

@Johan Commelin By the way, this is how I want high powered libraries to work

view this post on Zulip Mario Carneiro (May 27 2019 at 16:40):

The main theorem is one line, and the rest is elementary unpacking

view this post on Zulip Kenny Lau (May 27 2019 at 16:41):

great

view this post on Zulip Kenny Lau (May 27 2019 at 16:41):

where should we put this lemma? it has some tricky dependencies...

view this post on Zulip Johan Commelin (May 27 2019 at 16:44):

@Mario Carneiro Sounds good... I want more high-powered libraries (-;

view this post on Zulip Johan Commelin (May 27 2019 at 16:45):

Also... if possible the elementary unpacking should be by tidy or by schoolkid or by elementary


Last updated: May 15 2021 at 23:13 UTC