exists_companion — Mathlib

English

There exists a bilinear map B : BilinMap R M N such that for all x,y ∈ M, Q(x+y) = Q(x) + Q(y) + B(x,y).

Русский

Существует билинейная форма B : BilinMap R M N такая, что для любых x,y ∈ M выполняется Q(x+y) = Q(x) + Q(y) + B(x,y).

LaTeX

$$∃ B : BilinMap R M N, ∀ x y, Q (x + y) = Q x + Q y + B x y$$

Lean4

theorem exists_companion : ∃ B : BilinMap R M N, ∀ x y, Q (x + y) = Q x + Q y + B x y :=
  Q.exists_companion'

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