ext — Mathlib

English

Two linear maps are equal if they agree on all basis vectors: If f1(b i) = f2(b i) for all i, then f1 = f2.

Русский

Две линейные отображения равны, если они совпадают на всех базисных векторах: если f1(b i) = f2(b i) для всех i, то f1 = f2.

LaTeX

$$$$ \forall i,\ f_1(b_i) = f_2(b_i) \Rightarrow f_1 = f_2 $$$$

Lean4

/-- Two linear maps are equal if they are equal on basis vectors. -/
theorem ext {f₁ f₂ : M →ₛₗ[σ] M₁} (h : ∀ i, f₁ (b i) = f₂ (b i)) : f₁ = f₂ :=
  by
  ext x
  rw [← b.linearCombination_repr x, Finsupp.linearCombination_apply, Finsupp.sum]
  simp only [map_sum, LinearMap.map_smulₛₗ, h]

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