mem_splitSupport_iff_nonzero — Mathlib

English

For l : (Σ i, αs i) →₀ M and i ∈ ι, i is in splitSupport(l) if and only if split l i ≠ 0.

Русский

Для l : (Σ i, αs i) →₀ M и i ∈ ι, i принадлежит splitSupport(l) тогда и только тогда, когда split l i ≠ 0.

LaTeX

$$$i \\in \\mathrm{splitSupport}(l) \\iff \\mathrm{split}(l,i) \\neq 0$$$

Lean4

theorem mem_splitSupport_iff_nonzero (i : ι) : i ∈ splitSupport l ↔ split l i ≠ 0 :=
  by
  classical
    rw [splitSupport, mem_image, Ne, ← support_eq_empty, ← Ne, ← Finset.nonempty_iff_ne_empty, split, comapDomain,
    Finset.Nonempty]
  simp only [Finset.mem_preimage, exists_and_right, exists_eq_right, mem_support_iff, Sigma.exists, Ne]

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