ext' — Mathlib

English

Two morphisms between LocallyRingedSpace objects are equal if their associated ShHom components agree.

Русский

Два гомоморфизма между объектами LocallyRingedSpace равны, если их компоненты ShHom совпадают.

LaTeX

$$$ \\forall \\{X Y\\}, \\{f g : X \\to Y\\}, f.toShHom = g.toShHom \\Rightarrow f = g $$$

Lean4

@[ext]
theorem ext' {X Y : LocallyRingedSpace.{u}} {f g : X ⟶ Y} (h : f.toShHom = g.toShHom) : f = g := by cases f; cases g;
  congr

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