English
If α ≃ β and predicates p and q are equivalent pointwise, then {a | p a} ≃ {b | q b}.
Русский
Если α ≃ β и предикаты p и q эквивалентны по точкам, то {a | p a} ≃ {b | q b}.
LaTeX
$$$$ { a : α // p a } \\simeq { b : β // q b } \n\\text{whenever } e : α \\simeq β \text{ and } \\forall a, p a \\leftrightarrow q (e a). $$$$
Lean4
/-- If `α` is equivalent to `β` and the predicates `p : α → Prop` and `q : β → Prop` are equivalent
at corresponding points, then `{a // p a}` is equivalent to `{b // q b}`.
For the statement where `α = β`, that is, `e : perm α`, see `Perm.subtypePerm`. -/
@[simps apply]
def subtypeEquiv {p : α → Prop} {q : β → Prop} (e : α ≃ β) (h : ∀ a, p a ↔ q (e a)) :
{ a : α // p a } ≃ { b : β // q b }
where
toFun a := ⟨e a, (h _).mp a.property⟩
invFun b := ⟨e.symm b, (h _).mpr ((e.apply_symm_apply b).symm ▸ b.property)⟩
left_inv a := Subtype.ext <| by simp
right_inv b := Subtype.ext <| by simp
