English
Let α be a type and p a predicate on α. If x is an element of the subtype {a ∈ α | p a}, then p holds for the underlying value of x.
Русский
Пусть α — множество и p — предикат на α. Если x является элементом подтипа {a ∈ α | p a}, то выполняется p для базового значения x.
LaTeX
$$$\forall \alpha \,(p : \alpha \to \mathrm{Prop}),\ \forall x \in \{a \in \alpha \mid p(a)\},\ p(x).$$$
Lean4
/-- A version of `x.property` or `x.2` where `p` is syntactically applied to the coercion of `x`
instead of `x.1`. A similar result is `Subtype.mem` in `Mathlib/Data/Set/Basic.lean`. -/
-- This is a leftover from Lean 3: it is identical to `Subtype.property`, and should be deprecated.
theorem prop (x : Subtype p) : p x :=
x.2
