apply_mem_span_image_iff_mem_span

English

Assume RingHomSurjective σ₁₂ and f is injective on the underlying maps. Then f x ∈ span_{R₂}(f''s) iff x ∈ span_R s.

Русский

Пусть существует сюрьекция RingHom σ₁₂ и отображение f инъективно; тогда f x ∈ span_{R₂}(f''s) эквивалентно x ∈ span_R s.

LaTeX

$$$$ f x \\in \\operatorname{span}_{R_2}(f''s) \\iff x \\in \\operatorname{span}_R s, $$$$

Lean4

theorem apply_mem_span_image_iff_mem_span [RingHomSurjective σ₁₂] {f : F} {x : M} {s : Set M}
    (hf : Function.Injective f) : f x ∈ Submodule.span R₂ (f '' s) ↔ x ∈ Submodule.span R s := by
  rw [← Submodule.mem_comap, ← Submodule.map_span, Submodule.comap_map_eq_of_injective hf]

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