ext — Mathlib

English

Two centroid homomorphisms are equal if they agree on every input; i.e., extensionality principle for CentroidHom.

Русский

Два центроид-гомоморфа равны, если они совпадают на каждом элементе; принцип экстентности для CentroidHom.

LaTeX

$$∀ {f g : CentroidHom α}, (∀ a, f a = g a) ⇒ f = g$$

Lean4

@[ext]
theorem ext {f g : CentroidHom α} (h : ∀ a, f a = g a) : f = g :=
  DFunLike.ext f g h

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