ext — Mathlib

English

Extensionality principle for morphisms in TopCat: two morphisms are equal if they agree on all inputs.

Русский

Принцип экстенсиональности морфизмов в TopCat: два морфизма равны, если они согласны на всех аргументах.

LaTeX

$$$\\forall X,Y \\ : \\ TopCat, \\forall f,g : X \\to Y,\\ (\\forall x : X,\\ f(x)=g(x)) \\Rightarrow f=g$$$

Lean4

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

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