proving a lemma about infinite sets

Stream: new members

[Anas Himmi]

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]

never mind i found it

[Jalex Stark]

Do you mind posting what you found?

[Anas Himmi]

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]

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

[Kevin Buzzard]

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

[Anas Himmi]

i see

[Jalex Stark]

i bet there are lemmas about infinite sets in flypitch?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Jalex Stark]

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]

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

[Mario Carneiro]

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]

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

[Gabriel Ebner]

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

[Gabriel Ebner]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Johan Commelin]

Or if and decidable_if?

[Mario Carneiro]

if should be decidable by default, like the term