subtypeEquivOfSubtype — Mathlib

English

If α ≃ β, then for any predicate p : β → Prop the subtype { a : α // p (e a) } is equivalent to { b : β // p b }.

Русский

Если α эквивалентно β, то для любого предиката p : β → Prop подтип { a : α // p (e a) } эквивалентен { b : β // p b }.

LaTeX

$$$( e : \\alpha \\simeq \\beta ) \\Rightarrow (\\{ a : \\alpha \\mid p (e a) \\} \\simeq \\{ b : \\beta \\mid p b \\})$$$

Lean4

/-- If `α ≃ β`, then for any predicate `p : β → Prop` the subtype `{a // p (e a)}` is equivalent
to the subtype `{b // p b}`. -/
def subtypeEquivOfSubtype {p : β → Prop} (e : α ≃ β) : { a : α // p (e a) } ≃ { b : β // p b } :=
  subtypeEquiv e <| by simp

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