ext — Mathlib

English

Two PEquiv α β are equal if they agree on all elements; extensionality principle for PEquiv.

Русский

Две псевдо-эквивалентности PEquiv α β равны, если их коэффициенты совпадают на всех элементах; принцип экстенсивности.

LaTeX

$$$$ \\forall x, f(x)=g(x) \\Rightarrow f=g. $$$$

Lean4

@[ext]
theorem ext {f g : α ≃. β} (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext f g h

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