ext — Mathlib

English

There is an extensional principle for partial maps: if the domain equality and the compatibility of the morphisms hold, then the partial maps are equal.

Русский

Существует принцип экстенсиональности для частичных карт: если выполняются равенство доменов и совместимость морфизмов, то частичные карты равны.

LaTeX

$$$$\\text{Ext }(f,g,e,H): f = g \\text{ if } f.domain = g.domain \\text{ and } f.hom = (X.isoOfEq e).hom \\circ g.hom.$$$$

Lean4

@[ext]
theorem ext (f g : X.PartialMap Y) (e : f.domain = g.domain) (H : f.hom = (X.isoOfEq e).hom ≫ g.hom) : f = g :=
  by
  rw [ext_iff]
  exact ⟨e, H⟩

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