mem_of_mem_span — Mathlib

English

If x lies in the span of e over H, and ε_i(x) ≠ 0 for some i, then i ∈ H.

Русский

Если x лежит в подмодуле span R (e '' H) и существует i с ε_i(x) ≠ 0, то i ∈ H.

LaTeX

$$$ \\forall H:\\,\\text{Set } ι,\\; \\forall x:\\, M,\\ x ∈ \\mathrm{span}_R(e''H) \\Rightarrow \\forall i, \\varepsilon_i x ≠ 0 \\Rightarrow i \\in H $$$

Lean4

theorem mem_of_mem_span {H : Set ι} {x : M} (hmem : x ∈ Submodule.span R (e '' H)) : ∀ i : ι, ε i x ≠ 0 → i ∈ H :=
  by
  intro i hi
  rcases (Finsupp.mem_span_image_iff_linearCombination _).mp hmem with ⟨l, supp_l, rfl⟩
  apply not_imp_comm.mp ((Finsupp.mem_supported' _ _).mp supp_l i)
  rwa [← lc_def, h.dual_lc] at hi

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