range_map_nonempty — Mathlib

English

For any submodule N of M, the set of images under all semilinear maps is nonempty; there exists some ϕ such that Submodule.map ϕ N is defined (nonempty).

Русский

Для любого подмодуля N ⊆ M существует образ под некоторым отображением; множество образов не пустое.

LaTeX

$$Nonempty (range (fun ϕ => Submodule.map ϕ N))$$

Lean4

theorem range_map_nonempty (N : Submodule R M) :
    (Set.range (fun ϕ => Submodule.map ϕ N : (M →ₛₗ[σ₁₂] M₂) → Submodule R₂ M₂)).Nonempty :=
  ⟨_, Set.mem_range.mpr ⟨0, rfl⟩⟩

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