hom_ext — Mathlib

English

Morphisms between bounded lattices are determined by their underlying functions; if two morphisms have the same underlying function, they are equal.

Русский

Гомоморфизмы между ограниченными решетками определяются своей подлежащей функцией; если две морфизмы имеют одну и ту же подлежащую функцию, они равны.

LaTeX

$$f.hom = g.hom → f = g$$

Lean4

@[ext]
theorem hom_ext {X Y : BddLat} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g :=
  Hom.ext hf

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