forall' — Mathlib

English

If p is a predicate on α depending on membership in s, then the forall' statement over the subset s is equivalent to the forall statement over s written in terms of elements of s.

Русский

Если предикат p зависит от принадлежности к s, то общий для всех над подтипом s эквивалентен всеобщему над элементами подтипа s.

LaTeX

$$$(\forall x : s, p x) \;\leftrightarrow\; \forall x : \alpha, p x.1 x.2$$

Lean4

theorem forall' {s : Set α} {p : ∀ x, x ∈ s → Prop} : (∀ (x) (h : x ∈ s), p x h) ↔ ∀ x : s, p x.1 x.2 :=
  (@SetCoe.forall _ _ fun x => p x.1 x.2).symm

Похожие утверждения