## Stream: general

### Topic: infinite sets

#### 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?

#### 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


#### Mario Carneiro (May 27 2019 at 16:13):

that's equivalent to a cardinal theorem

#### Kenny Lau (May 27 2019 at 16:14):

how many lines would I need?

#### 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


#### Kenny Lau (May 27 2019 at 16:34):

14 lines without cardinal

#### 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


#### 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

#### Mario Carneiro (May 27 2019 at 16:39):

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

#### Mario Carneiro (May 27 2019 at 16:40):

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

great

#### Kenny Lau (May 27 2019 at 16:41):

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

#### Johan Commelin (May 27 2019 at 16:44):

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

#### 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