isoCongrRight — Mathlib

English

If Y1 is isomorphic to Y2, there is a bijection between Iso(X,Y1) and Iso(X,Y2).

Русский

Если Y1 изоморфен Y2, существует биекция между Iso(X,Y1) и Iso(X,Y2).

LaTeX

$$$ \\text{IsoCongrRight}(g) : (X \\cong Y_1) \\simeq (X \\cong Y_2)$$$

Lean4

/-- If `Y₁` is isomorphic to `Y₂`, then there is a bijection between `X ≅ Y₁` and `X ≅ Y₂`. -/
def isoCongrRight {X Y₁ Y₂ : C} (g : Y₁ ≅ Y₂) : (X ≅ Y₁) ≃ (X ≅ Y₂) :=
  isoCongr (Iso.refl _) g

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