English
Characterization of membership in ϕ.submoduleImage N: x ∈ ϕ.submoduleImage N iff there exists y with y ∈ N and φ y = x.
Русский
Условия принадлежности x к ϕ.submoduleImage N: x ∈ ϕ.submoduleImage N тогда и только тогда, когда существует y ∈ N такое что φ y = x.
LaTeX
$$$$ x \in \varphi.\mathrm{submoduleImage }N \iff \exists y \in N: \varphi(y) = x $$$$
Lean4
@[simp]
theorem mem_submoduleImage {M' : Type*} [AddCommMonoid M'] [Module R M'] {O : Submodule R M} {ϕ : O →ₗ[R] M'}
{N : Submodule R M} {x : M'} : x ∈ ϕ.submoduleImage N ↔ ∃ (y : _) (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x :=
by
refine Submodule.mem_map.trans ⟨?_, ?_⟩ <;> simp_rw [Submodule.mem_comap]
· rintro ⟨⟨y, yO⟩, yN : y ∈ N, h⟩
exact ⟨y, yO, yN, h⟩
· rintro ⟨y, yO, yN, h⟩
exact ⟨⟨y, yO⟩, yN, h⟩
