subtypeEquivOfSubtype' — Mathlib

English

If α ≃ β, then { a : α // p a } ≃ { b : β // p (e.symm b) }. This version is used by equiv_rw.

Русский

Если α ≃ β, то { a : α // p a } ≃ { b : β // p (e.symm b) }. Этот вариант используется в equiv_rw.

LaTeX

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

Lean4

/-- If `α ≃ β`, then for any predicate `p : α → Prop` the subtype `{a // p a}` is equivalent
to the subtype `{b // p (e.symm b)}`. This version is used by `equiv_rw`. -/
def subtypeEquivOfSubtype' {p : α → Prop} (e : α ≃ β) : { a : α // p a } ≃ { b : β // p (e.symm b) } :=
  e.symm.subtypeEquivOfSubtype.symm

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