English
Let s be a subset of α and p a predicate on s. Then (for all x in s, p x) is equivalent to (for all x in α with x ∈ s, p ⟨x, h⟩) where ⟨x, h⟩ is the element of the subtype corresponding to x and the proof h that x ∈ s.
Русский
Пусть s ⊆ α и p — предикат над s. Тогда (для всех x из s выполняется p x) эквивалентно (для всех x из α при условии x ∈ s следует p ⟨x, h⟩), где ⟨x, h⟩ — элемент подтипа, соответствующий x и доказательству x ∈ s.
LaTeX
$$$(\forall x : s, p\,x) \;\iff\; \forall x (h : x \in s),\; p\langle x, h \rangle$$$
Lean4
theorem «forall» {s : Set α} {p : s → Prop} : (∀ x : s, p x) ↔ ∀ (x) (h : x ∈ s), p ⟨x, h⟩ :=
Subtype.forall
