Zulip Chat Archive

Stream: maths

Topic: Infinite sets are nonempty


view this post on Zulip Ryan Lahfa (Apr 04 2020 at 21:27):

If I look at this theorem:

lemma infinite_set_is_not_empty (S: set X): set.infinite S  S.nonempty

I'm not sure why it does not exist, maybe it's false but I don't really see why as infinite definition is not finite.

And I can give this proof in Lean:

import data.set

lemma infinite_set_is_not_empty (S: set X): set.infinite S  S.nonempty :=
begin
intro h,
by_contra,
rw set.not_nonempty_iff_eq_empty at a,
apply h,
rw a,
exact set.finite_empty,
end

view this post on Zulip Ryan Lahfa (Apr 04 2020 at 21:28):

(under the assumption of decidability, so I guess, noncomputable theory and open_locale classical are needed.)

view this post on Zulip Scott Morrison (Apr 05 2020 at 01:49):

import data.fintype.basic

example {X : Type} [infinite X] : nonempty X :=
by apply_instance

view this post on Zulip Scott Morrison (Apr 05 2020 at 01:50):

This is not a statement about sets, but about types.

view this post on Zulip Kevin Buzzard (Apr 05 2020 at 08:45):

Note that set.nonempty is not a class, but nonempty is.

view this post on Zulip Ryan Lahfa (Apr 05 2020 at 09:37):

@Scott Morrison But this is not really about my example, should I use subtypes to apply it to a subset of X?


Last updated: May 18 2021 at 08:14 UTC