## Stream: new members

### Topic: forall_exists_index

#### Vivek Rajesh Joshi (Sep 09 2023 at 06:14):

Can anyone explain to me what this theorem does (explanation of its proof is not needed), and how it is getting applied in this context?

∃ x, (∀ (i : I), x ∈ A i) ∧ f x = y iff ∀ (x : α), (∀ (i : I), x ∈ A i) ∧ f x = y

#### Kevin Buzzard (Sep 09 2023 at 06:20):

Can you post a #mwe so we can run the code on our own computer with little effort (and in particular understand the types of the terms involved in your statement)? You ask about a theorem being applied but as far as I can see you're just writing down a true/false statement, there is no proof or application

#### Kevin Buzzard (Sep 09 2023 at 06:21):

It would be like me writing 2+2=5 and asking how it is getting applied

#### Eric Wieser (Sep 09 2023 at 06:23):

docs#forall_exists_index

#### Kevin Buzzard (Sep 09 2023 at 06:25):

Oh I see, the clue is in the title (which is a lot less prominent on the mobile app). I still don't understand the question though, where's the application?

#### Vivek Rajesh Joshi (Sep 09 2023 at 08:00):

Kevin Buzzard said:

Oh I see, the clue is in the title (which is a lot less prominent on the mobile app). I still don't understand the question though, where's the application?

Sorry, I'll keep that in mind next time.
The line I have written is part of a proof for a theorem. The goal had the expression on the LHS, and simp converted it to the expression in the RHS. After typing simp?, I realised that it used the theorem forall_exists_index to do this. I am unable to understand how this theorem was used here, and why the conversion makes sense.

#### Kevin Buzzard (Sep 09 2023 at 08:43):

Then post a #mwe (that's a link)

#### Vivek Rajesh Joshi (Sep 09 2023 at 09:55):

import Mathlib.Tactic
import Mathlib.Data.Set.Lattice
import Mathlib.Data.Set.Function
import Mathlib.Analysis.SpecialFunctions.Log.Basic

variable {α β : Type _}
variable (f : α → β)
variable (s t : Set α)
variable (u v : Set β)

open Function
open Set

variable {I : Type _} (A : I → Set α) (B : I → Set β)

example : (f '' ⋂ i, A i) ⊆ ⋂ i, f '' A i := by
intro y; simp
intro x h fxeq i
use x
exact ⟨h i, fxeq⟩


#### Kevin Buzzard (Sep 09 2023 at 14:15):

Yeah so simp? reports that it uses forall_exists_index. We can take the simp call apart a bit more and see exactly what it's doing:

import Mathlib.Tactic

variable {α β : Type _}
variable (f : α → β)
variable (s t : Set α)
variable (u v : Set β)

open Function
open Set

variable {I : Type _} (A : I → Set α) (B : I → Set β)

#check forall_exists_index
/-
forall_exists_index.{u_1} {α : Sort u_1} {p : α → Prop} {q : (∃ x, p x) → Prop} :
(∀ (h : ∃ x, p x), q h) ↔ ∀ (x : α) (h : p x), q (_ : ∃ x, p x)
-/

example : (f '' ⋂ i, A i) ⊆ ⋂ i, f '' A i := by
intro y;
simp [-forall_exists_index] -- don't use it yet
-- ⊢ (∃ x, (∀ (i : I), x ∈ A i) ∧ f x = y) → ∀ (i : I), ∃ x, x ∈ A i ∧ f x = y
rw [forall_exists_index]
-- ⊢ ∀ (x : α), (∀ (i : I), x ∈ A i) ∧ f x = y → ∀ (i : I), ∃ x, x ∈ A i ∧ f x = y
simp
intro x h fxeq i
use x
exact ⟨h i, fxeq⟩


So before the application of forall_exists_index the goal is (there exists x such that P x) -> Q, and after the application it's (for all x, P x -> Q), and that's what the lemma says (actually the lemma says something slightly more general but what the heck) so that's what it's doing.

#### Vivek Rajesh Joshi (Sep 09 2023 at 14:38):

I understand what simp is doing, it is just rewriting the LHS of the lemma as the RHS. I just can't wrap my head around why that replacement makes sense, and what q and h are in this case.

#### Kevin Buzzard (Sep 09 2023 at 14:49):

In the application, h is a proof of (∃ x, (∀ (i : I), x ∈ A i) ∧ f x = y) and q is the function which eats h, ignores it (which is why I said that the lemma was more general than needed) and returns a proof of ∀ (i : I), ∃ x, x ∈ A i ∧ f x = y (a statement which doesn't depend on h).

Last updated: Dec 20 2023 at 11:08 UTC