ext — Mathlib

English

Two AddConstEquiv G H a b are equal if they agree on every input x ∈ G; i.e., if for all x, e1 x = e2 x, then e1 = e2.

Русский

Два AddConstEquiv G H a b равны, если они совпадают на каждом элементе x ∈ G; то есть если для всех x выполняется e1 x = e2 x, то e1 = e2.

LaTeX

$$$ (\forall x:\, G, e_1 x = e_2 x) \Rightarrow e_1 = e_2 $$$

Lean4

@[ext]
theorem ext {e₁ e₂ : G ≃+c[a, b] H} (h : ∀ x, e₁ x = e₂ x) : e₁ = e₂ :=
  DFunLike.ext _ _ h

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