ext — Mathlib

English

Two VertexOperators are equal if they agree on every input vector; the ext principle holds for VertexOperator.

Русский

Два VertexOperator равны, если они согласованы на каждом векторе; применяется принцип экст.

LaTeX

$$$\forall A,B:\ VertexOperator(R,V),\ (\forall v:\ V, A v = B v) \Rightarrow A = B$$$

Lean4

@[ext]
theorem ext (A B : VertexOperator R V) (h : ∀ v : V, A v = B v) : A = B :=
  LinearMap.ext h

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