ext — Mathlib

English

Two morphisms between FinBddDistLat are equal if they agree on every element.

Русский

Два морфизма между FinBddDistLat равны, если совпадают на каждом элементе.

LaTeX

$$theorem ext {X Y : FinBddDistLat} {f g : FinBddDistLat.instCategory.Hom X Y} (w : ∀ x : X, f x = g x) : f = g$$

Lean4

@[ext]
theorem ext {X Y : FinBddDistLat} {f g : X ⟶ Y} (w : ∀ x : X, f x = g x) : f = g :=
  ConcreteCategory.hom_ext _ _ w

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