map_inl — Mathlib

English

For any submodule p of M, the image of p under the injection inl into M × M₂ equals the product p × ⊥.

Русский

Для подмодуля p ⊆ M образ под инъекцией inl в M × M₂ равен p × ⊥.

LaTeX

$$$\\mathrm{map}(\\mathrm{inl}\\, R\\, M\\, M_2)(p) = p \\times \\bot$$$

Lean4

@[simp]
theorem map_inl : p.map (inl R M M₂) = prod p ⊥ := by
  ext ⟨x, y⟩
  simp only [and_left_comm, eq_comm, mem_map, Prod.mk_inj, inl_apply, mem_bot, exists_eq_left', mem_prod]

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