subtypeOpEquiv — Mathlib

English

There is a natural equivalence between Subtype P.op and Subtype P.

Русский

Существует естественное эквивалентство между Subtype(P.op) и Subtype(P).

LaTeX

$$$\mathrm{Subtype}(P^{\mathrm{op}}) \simeq \mathrm{Subtype}(P)$$$

Lean4

/-- The bijection `Subtype P.op ≃ Subtype P` for `P : ObjectProperty C`. -/
def subtypeOpEquiv (P : ObjectProperty C) : Subtype P.op ≃ Subtype P
    where
  toFun x := ⟨x.1.unop, x.2⟩
  invFun x := ⟨op x.1, x.2⟩

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