English
For a finite set s ⊆ α and a predicate p on s, the universal quantification over the elements of s is equivalent to a universal quantification over all elements of α, provided we carry along the witness that the element lies in s.
Русский
Для конечного множества s ⊆ α и предиката p на s все элементы s удовлетворяют p эквивалентно тому, что для всех a ∈ α выполняется p(a) при условии a ∈ s и соответствующего доказательства.
LaTeX
$$∀ {α : Type*} (s : Finset α) (p : s → Prop), (∀ x : s, p x) ↔ ∀ (x : α) (h : x ∈ s), p ⟨x, h⟩$$
Lean4
protected theorem forall_coe {α : Type*} (s : Finset α) (p : s → Prop) :
(∀ x : s, p x) ↔ ∀ (x : α) (h : x ∈ s), p ⟨x, h⟩ :=
Subtype.forall
