English
An alternative version of Subtype.forall: for any q : ∀ x, p x → Prop, the universal quantification (∀ 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
$$$$(\forall x\ h,\ q\ x\ h) \iff \forall x : \{ a // p a \},\ q\ x\ x.2$$$$
Lean4
/-- An alternative version of `Subtype.forall`. This one is useful if Lean cannot figure out `q`
when using `Subtype.forall` from right to left. -/
protected theorem forall' {q : ∀ x, p x → Prop} : (∀ x h, q x h) ↔ ∀ x : { a // p a }, q x x.2 :=
(@Subtype.forall _ _ fun x ↦ q x.1 x.2).symm
