ext_basis — Mathlib

English

Two bilinear maps are equal if they agree on all pairs of basis vectors.

Русский

Два билинейных отображения равны, если они совпадают на всех парах базисных векторов.

LaTeX

$$ext_basis {B B' : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (h : ∀ i j, B (b₁ i) (b₂ j) = B' (b₁ i) (b₂ j)) : B = B'$$

Lean4

/-- Two bilinear maps are equal when they are equal on all basis vectors. -/
theorem ext_basis {B B' : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P} (h : ∀ i j, B (b₁ i) (b₂ j) = B' (b₁ i) (b₂ j)) : B = B' :=
  b₁.ext fun i => b₂.ext fun j => h i j

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