English
Let p and q be predicates on α with p x iff q x for all x. Then the subtypes { x : α | p x } and { x : α | q x } are canonically equivalent.
Русский
Пусть p и q – предикаты на α such that p x ↔ q x для всех x. Тогда подтипы { x ∈ α | p x } и { x ∈ α | q x } эквивалентны по естественному изоморфизму.
LaTeX
$$$\\left( \\forall x,\\ p x \\leftrightarrow q x \\right) \\Rightarrow \\left\\{ x : \\alpha \\mid p x \\right\\} \\simeq \\left\\{ x : \\alpha \\mid q x \\right\\} $$$
Lean4
/-- If two predicates `p` and `q` are pointwise equivalent, then `{x // p x}` is equivalent to
`{x // q x}`. -/
@[simps!]
def subtypeEquivRight {p q : α → Prop} (e : ∀ x, p x ↔ q x) : { x // p x } ≃ { x // q x } :=
subtypeEquiv (Equiv.refl _) e
