isoCongrLeft — Mathlib

English

If X1 is isomorphic to X2, there is a bijection between Iso(X1,Y) and Iso(X2,Y).

Русский

Если X1 изоморфен X2, существует биективное соответствие между Iso(X1,Y) и Iso(X2,Y).

LaTeX

$$$ \\text{IsoCongrLeft}(f) : (X_1 \\cong Y) \\simeq (X_2 \\cong Y)$$$

Lean4

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

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