mem_support_iff — Mathlib

English

The i-th component is nonzero exactly when the i-th projection of r is nonzero, i.e., i belongs to the support of the decomposition iff proj_i(r) ≠ 0.

Русский

Компонента i не равна нулю тогда и только тогда, когда i-я компонента проекции r не равна нулю; то есть i ∈ supp(decompose 𝒜 r) ⇔ proj 𝒜 i r ≠ 0.

LaTeX

$$$i \in \mathrm{supp}(\mathrm{decompose} 𝒜 r) \;\Leftrightarrow\; \mathrm{proj} 𝒜 i(r) \neq 0.$$$

Lean4

theorem mem_support_iff [DecidableEq A] (r : A) (i : ι) : i ∈ (decompose 𝒜 r).support ↔ GradedAlgebra.proj 𝒜 i r ≠ 0 :=
  DFinsupp.mem_support_iff.trans Submodule.coe_eq_zero.not.symm

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