ext_iff — Mathlib

English

Two partial maps f and g are equal iff there exists an equality of their domains and a canonical isomorphism equating their maps.

Русский

Две частичные карты f и g равны тогда и только тогда, когда существует равенство их доменов и каноническое изоморфирование, переводя одну карту в другую.

LaTeX

$$$$f = g \\iff \\exists e: f.domain = g.domain,\\; f.hom = (X.isoOfEq e).hom \\circ g.hom.$$$$

Lean4

theorem ext_iff (f g : X.PartialMap Y) : f = g ↔ ∃ e : f.domain = g.domain, f.hom = (X.isoOfEq e).hom ≫ g.hom :=
  by
  constructor
  · rintro rfl
    simp only [exists_true_left, Scheme.isoOfEq_rfl, Iso.refl_hom, Category.id_comp]
  · obtain ⟨U, hU, f⟩ := f
    obtain ⟨V, hV, g⟩ := g
    rintro ⟨rfl : U = V, e⟩
    congr 1
    simpa using e

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