ext — Mathlib

English

Elements of a function (or module) are equal if all their coordinates are equal: if ∀ i, x i = y i, then x = y.

Русский

Элементы функции (или модуля) равны, если все их координаты равны: если ∀ i, x_i = y_i, то x = y.

LaTeX

$$$$ (\\forall i, x(i) = y(i)) \\Rightarrow x = y $$$$

Lean4

@[ext]
theorem ext (𝕜 : Type u) (A : Type v) [NontriviallyNormedField 𝕜] [NonUnitalNormedRing A] [NormedSpace 𝕜 A]
    [SMulCommClass 𝕜 A A] [IsScalarTower 𝕜 A A] (a b : 𝓜(𝕜, A)) (h : a.toProd = b.toProd) : a = b :=
  by
  cases a
  cases b
  simpa using h

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