forall_coord_eq_zero_iff — Mathlib

English

Let b be a basis of a module M. Then an element x ∈ M is zero if and only if all its coordinates with respect to b are zero; i.e., x = 0 ⇔ ∀ i, b.coord i x = 0.

Русский

Пусть b является базисом модуля M. Тогда вектор x ∈ M равен нулю тогда, когда все его координаты по базису b равны нулю; то есть x = 0 тогда и только тогда, когда ∀ i, b.coord i x = 0.

LaTeX

$$$\forall x \in M\, (\forall i, b.coord\,i\, x = 0) \iff x = 0$$$

Lean4

theorem forall_coord_eq_zero_iff {x : M} : (∀ i, b.coord i x = 0) ↔ x = 0 :=
  Iff.trans (by simp only [b.coord_apply, DFunLike.ext_iff, Finsupp.zero_apply]) b.repr.map_eq_zero_iff

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