mem_map — Mathlib

English

Characterization of membership in the image: an element lies in the image of N under f iff it is the image of some element of N.

Русский

Утверждение о принадлежности образу: элемент лежит в образе N под действием f тогда и только тогда, когда он является образцом некоторого элемента N.

LaTeX

$$$ m' \in N.map f \iff \exists m, m \in N \land f m = m' $$$

Lean4

@[simp]
theorem mem_map (m' : M') : m' ∈ N.map f ↔ ∃ m, m ∈ N ∧ f m = m' :=
  Submodule.mem_map

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