infinite sets

Stream: general

[Kenny Lau]

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

[Kenny Lau]

for example:

theorem set.of_not_finite {s : set α} (hfs : ¬s.finite) :
  ∃ f : ℕ → α, function.injective f ∧ ∀ n, f n ∈ s :=
sorry

[Mario Carneiro]

that's equivalent to a cardinal theorem

[Kenny Lau]

how many lines would I need?

[Kenny Lau]

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

[Kenny Lau]

14 lines without cardinal

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kenny Lau]

great

[Kenny Lau]

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

[Johan Commelin]

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

[Johan Commelin]

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