Infinite sets are nonempty

Stream: maths

[Ryan Lahfa]

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

[Ryan Lahfa]

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

[Scott Morrison]

import data.fintype.basic

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

[Scott Morrison]

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

[Kevin Buzzard]

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

[Ryan Lahfa]

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