Exists from forall

Stream: new members

[VayusElytra]

A stupid question, suppose you have a situation like the following:

lemma SomeLemma (N : Set ℕ) (P : ℕ → Prop) (h : (∀ x ∈ N, P x)) : (∃ x ∈ N, P x) := by
  sorry

How can you extract one element of N to prove this theorem?

[Nick Attkiss]

I think you need to assume that N is nonempty to prove this, otherwise the forall statement can hold vacuously while the exists statement is false

[VayusElytra]

My bad, it definitely needs that extra assumption. To make it more in line with what I am working on:

lemma SomeLemma (N : Set ℕ) (h₁ : N ∈ atTop) (P : ℕ → Prop) (h : (∀ x ∈ N, P x)) : (∃ x ∈ N, P x) := by
  sorry

N in atTop should guarantee non-emptiness.

[Etienne Marion]

Using docs#Filter.nonempty_of_mem you get N.Nonempty, which you can destruct into an element in N. Then you can just apply h to this element.

[VayusElytra]

Thank you, that worked perfectly :)