forall_exists_index

Stream: new members

[Vivek Rajesh Joshi]

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]

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]

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

[Eric Wieser]

docs#forall_exists_index

[Kevin Buzzard]

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]

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]

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

[Vivek Rajesh Joshi]

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]

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]

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]

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).