## Stream: new members

### Topic: proving a lemma about infinite sets

#### Anas Himmi (May 05 2020 at 14:46):

how to prove this?

example (α : Type*) (U: set α) (h:set.infinite U) (x: α)  : ∃ z∈U,z≠x := _


any help appreciated :grinning_face_with_smiling_eyes:

#### Anas Himmi (May 05 2020 at 15:07):

never mind i found it

#### Jalex Stark (May 05 2020 at 16:09):

Do you mind posting what you found?

#### Anas Himmi (May 05 2020 at 16:16):

of course

lemma exists_neq_of_infinite {α : Type u} {U: set α} (h:set.infinite U) (x: α)  : ∃ z∈U,z≠x :=
or.elim (classical.em (x∈U))
(λ 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⟩))


#### Anas Himmi (May 05 2020 at 16:18):

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

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

i see

#### Jalex Stark (May 05 2020 at 17:23):

i bet there are lemmas about infinite sets in flypitch?

#### Mario Carneiro (May 05 2020 at 17:38):

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

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

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

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

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


#### Mario Carneiro (May 05 2020 at 17:49):

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

#### Gabriel Ebner (May 05 2020 at 18:04):

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

#### Gabriel Ebner (May 05 2020 at 18:04):

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

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

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

#### Mario Carneiro (May 05 2020 at 18:07):

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

#### Mario Carneiro (May 05 2020 at 18:09):

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

#### Johan Commelin (May 05 2020 at 18:09):

Or if and decidable_if?

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