notMem_span_of_apply_notMem_span_image

English

If f x ∉ span_{R₂}(f''s) then x ∉ span_R s (contrapositive of image-span membership).

Русский

Если f x не принадлежит span_{R₂}(f''s), то x не принадлежит span_R s (контрапозиция к существованию образа).

LaTeX

$$$$ f x \\notin \\operatorname{span}_{R_2}(f''s) \\Rightarrow x \\notin \\operatorname{span}_R s. $$$$

Lean4

/-- `f` is an explicit argument so we can `apply` this theorem and obtain `h` as a new goal. -/
theorem notMem_span_of_apply_notMem_span_image [RingHomSurjective σ₁₂] (f : F) {x : M} {s : Set M}
    (h : f x ∉ Submodule.span R₂ (f '' s)) : x ∉ Submodule.span R s :=
  h.imp (apply_mem_span_image_of_mem_span f)

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