English
An alternative version of Subtype.exists: given q : ∀ x, p x → Prop, the existence statement (∃ x h, q x h) is equivalent to ∃ x : { a // p a }, q x x.2.
Русский
Альтернативная формулировка для существования в подтипе: для q : ∀ x, p x → Prop, существование (∃ x h, q x h) эквивалентно ∃ x : { a // p a }, q x x.2.
LaTeX
$$$$(\exists x\ h,\ q\ x\ h) \iff \exists x : \{ a // p a \},\ q\ x x.2$$$$
Lean4
/-- An alternative version of `Subtype.exists`. This one is useful if Lean cannot figure out `q`
when using `Subtype.exists` from right to left. -/
protected theorem exists' {q : ∀ x, p x → Prop} : (∃ x h, q x h) ↔ ∃ x : { a // p a }, q x x.2 :=
(@Subtype.exists _ _ fun x ↦ q x.1 x.2).symm
