Zulip Chat Archive

Stream: new members

Topic: proving a lemma about infinite sets


view this post on Zulip Anas Himmi (May 05 2020 at 14:46):

how to prove this?

example (α : Type*) (U: set α) (h:set.infinite U) (x: α)  :  zU,zx := _

any help appreciated :grinning_face_with_smiling_eyes:

view this post on Zulip Anas Himmi (May 05 2020 at 15:07):

never mind i found it

view this post on Zulip Jalex Stark (May 05 2020 at 16:09):

Do you mind posting what you found?

view this post on Zulip Anas Himmi (May 05 2020 at 16:16):

of course

lemma exists_neq_of_infinite {α : Type u} {U: set α} (h:set.infinite U) (x: α)  :  zU,zx :=
or.elim (classical.em (xU))
(λ ho,let y,hy,hy':=exists_of_ssubset (ssubset_iff_subset_ne.mpr singleton_subset_iff.mpr ho,λ hh,(hh.symm  h) (finite_singleton x))
in y,hy,finset.not_mem_singleton.mp hy')
(λ ho,have hh:U.nonempty,from or.elim (eq_empty_or_nonempty U) (λ hh,by rw hh at h;exact (false.elim (h finite_empty))) id,exists.elim hh
(λ y hy,y,hy,by finish))

view this post on Zulip Anas Himmi (May 05 2020 at 16:18):

honestly i was surprised to find so few lemmas about infinite sets in mathlib

view this post on Zulip Kevin Buzzard (May 05 2020 at 16:25):

Finite sets are the important sets in mathematics. You can't prove anything without some sort of control over your objects

view this post on Zulip Anas Himmi (May 05 2020 at 16:30):

i see

view this post on Zulip Jalex Stark (May 05 2020 at 17:23):

i bet there are lemmas about infinite sets in flypitch?

view this post on Zulip Mario Carneiro (May 05 2020 at 17:38):

flypitch is mostly doing transfinite set theory, which isn't quite the same

view this post on Zulip Mario Carneiro (May 05 2020 at 17:39):

set.infinite is best understood as the negation of set.finite. Try to prove this theorem by contrapositive

view this post on Zulip Jalex Stark (May 05 2020 at 17:41):

I see, so the proof I had in mind would look like "use choice, you're in bijection with an infinite cardinal, use facts about cardinals", but that's obviously overkill

view this post on Zulip Mario Carneiro (May 05 2020 at 17:42):

Those theorems should be there in set_theory.cardinal if you want to go that route though

view this post on Zulip Mario Carneiro (May 05 2020 at 17:48):

lemma exists_neq_of_infinite {α} {U : set α} (h : set.infinite U) (x : α) :  z  U, z  x :=
begin
  classical, by_contra H, apply h,
  apply set.finite_subset (set.finite_singleton x),
  push_neg at H, simpa [set.subset_def] using H
end

view this post on Zulip Mario Carneiro (May 05 2020 at 17:49):

Can I vote for by_contra! to do contradiction without a decidable assumption?

view this post on Zulip Gabriel Ebner (May 05 2020 at 18:04):

There is also by_cases!. Or as I would like to call it, by_cases.

view this post on Zulip Gabriel Ebner (May 05 2020 at 18:04):

If somebody submits a PR to core, I think we should this.

view this post on Zulip Mario Carneiro (May 05 2020 at 18:05):

Would it be too expensive to search for a decidable instance first, and then fall back on a classical proof?

view this post on Zulip Mario Carneiro (May 05 2020 at 18:06):

I'm not usually a fan of exploratory typeclass inference because it's a waste of time if the search is going to fail

view this post on Zulip Mario Carneiro (May 05 2020 at 18:07):

How about renaming by_cases! to by_cases and by_cases to if?

view this post on Zulip Mario Carneiro (May 05 2020 at 18:09):

(even better if it literally uses dite instead of decidable.by_cases)

view this post on Zulip Johan Commelin (May 05 2020 at 18:09):

Or if and decidable_if?

view this post on Zulip Mario Carneiro (May 05 2020 at 18:10):

if should be decidable by default, like the term


Last updated: May 06 2021 at 22:13 UTC