ext — Mathlib

English

Equality in PiLp p α is determined coordinatewise: two elements are equal if and only if they agree at every coordinate.

Русский

Равенство в PiLp p α задается координатно: два элемента равны тогда и только тогда, когда они согласованы на каждой координате.

LaTeX

$$$\\forall x,y:\\; (\\forall i, x_i=y_i) \\Rightarrow x=y$$$

Lean4

@[ext]
protected theorem ext {p : ℝ≥0∞} {ι : Type*} {α : ι → Type*} {x y : PiLp p α} (h : ∀ i, x i = y i) : x = y :=
  funext h

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