ext — Mathlib

English

Two absolute value maps are equal iff they coincide on every element: extensionality principle.

Русский

Две отображения абсолютного значения равны тогда и только тогда, когда они совпадают на каждом элементе.

LaTeX

$$$\forall f,g:\;\text{AbsoluteValue}(R,S),\ (\forall x:\; f(x)=g(x))\Rightarrow f=g$$$

Lean4

@[ext]
theorem ext ⦃f g : AbsoluteValue R S⦄ : (∀ x, f x = g x) → f = g :=
  DFunLike.ext _ _

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