Dealing with "partial" functions

Stream: new members

[Nir Paz]

If I have a function of type similar to Π x < b, α, how can I easily state that an element is in its range?

For example I want H to be the assumption that there is some i < 7 that is sent to 0, and the ways I found are silly:

import Mathlib

-- stupid
example (f : Π n < 7, ℕ) (H : ∃ i < 7, ((h : i < 7) → f i h = 0)) : True := trivial

-- stupider
example (f : Π n < 7, ℕ) (H : ∃ i, Nonempty ((h : i < 7) ×' (f i h = 0))) : True := trivial

[Kyle Miller]

∃ i < 7, ((h : i < 7) → f i h = 0) isn't stated right, since the implication makes it be trivially true (use i = 7 for example).

You can write (H : ∃ (i : ℕ) (h : i < 7), f i h = 0) for a "dependent conjunction". If you don't want the type ascription, you can also write ∃ i, ∃ (h : i < 7), f i h = 0 by splitting the existential.

[Kyle Miller]

I think the summary is that the existential is how you write Nonempty (... ×' ...)

[Nir Paz]

Just found the theorem I was proving in mathlib and they use ∃ i h, f i h = 0, thanks!