hom_ext — Mathlib

English

Morphisms between bounded lattices are determined by their action on points; if two morphisms agree on all points, they are equal.

Русский

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

LaTeX

$$theorem hom_ext {X Y : BddLat} {f g : X ⟶ Y} (hf : f.hom = g.hom) : f = g$$

Lean4

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

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