mem_map — Mathlib

English

Pushing forward along a composition equals successive pushes forward: I.map(g'.comp g) = (I.map g).map g'.

Русский

Перемещение вдоль композиции равно последовательному переносу: I.map(g'∘g) = (I.map g).map g'.

LaTeX

$$I.map (g'.comp g) = (I.map g).map g'$$

Lean4

@[simp]
theorem mem_map {I : FractionalIdeal S P} {g : P →ₐ[R] P'} {y : P'} : y ∈ I.map g ↔ ∃ x, x ∈ I ∧ g x = y :=
  Submodule.mem_map

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