mem_submoduleImage_of_le — Mathlib

English

If N ≤ O, then x ∈ φ.submoduleImage N iff ∃ y ∈ N with φ ⟨y, hNO yN⟩ = x.

Русский

Если N ≤ O, то x ∈ φ.submoduleImage N эквивалентно существованию y ∈ N such that φ ⟨y, hNO yN⟩ = x.

LaTeX

$$$$ x \in \varphi.\mathrm{submoduleImage }N \iff \exists y \in N: \varphi(⟨y, hNO yN⟩) = x $$$$

Lean4

theorem mem_submoduleImage_of_le {M' : Type*} [AddCommMonoid M'] [Module R M'] {O : Submodule R M} {ϕ : O →ₗ[R] M'}
    {N : Submodule R M} (hNO : N ≤ O) {x : M'} : x ∈ ϕ.submoduleImage N ↔ ∃ (y : _) (yN : y ∈ N), ϕ ⟨y, hNO yN⟩ = x :=
  by grind [mem_submoduleImage]

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