isoOfEqMk — Mathlib

English

Equality mk f = X yields an isomorphism between the underlying objects A and X.

Русский

Равенство mk f = X порождает изоморфизм между A и X.

LaTeX

$$$\text{isoOfMkEq } f X h : A \cong X$$$

Lean4

/-- An equality of subobjects gives an isomorphism of the corresponding objects. -/
@[simps]
def isoOfEqMk {B A : C} (X : Subobject B) (f : A ⟶ B) [Mono f] (h : X = mk f) : (X : C) ≅ A
    where
  hom := ofLEMk X f h.le
  inv := ofMkLE f X h.ge

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