spanFinset_eq_zero — Mathlib

English

spanFinset R s f = 0 if and only if all f(j) = 0 for j in s.

Русский

spanFinset R s f равно нулю тогда и только тогда, когда все значения f(j) равны нулю на каждом j ∈ s.

LaTeX

$$$ \operatorname{spanFinset} R\, s\, f = 0 \iff \forall j \in s,\; f(j) = 0 $$$

Lean4

@[simp]
theorem spanFinset_eq_zero {ι : Type*} {s : Finset ι} {f : ι → K} : spanFinset R₁ s f = 0 ↔ ∀ j ∈ s, f j = 0 := by
  simp only [← coeToSubmodule_inj, spanFinset_coe, coe_zero, Submodule.span_eq_bot, Set.mem_image, Finset.mem_coe,
    forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]

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