# Zulip Chat Archive

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

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

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