map_id — Mathlib

English

If p ⊆ p' and q ⊆ q', then the range of mapIncl p q is contained in the range of mapIncl p' q'.

Русский

Если p ⊆ p' и q ⊆ q', то образ отображения mapIncl p q содержится в образе mapIncl p' q'.

LaTeX

$$$p \\leq p' \\;\\&\\; q \\leq q' \\Rightarrow \\operatorname{range}(\\mathrm{mapIncl}\\ p\\ q) \\leq \\operatorname{range}(\\mathrm{mapIncl}\\ p'\\ q')$$$

Lean4

@[simp]
theorem map_id : map (id : M →ₗ[R] M) (id : N →ₗ[R] N) = .id :=
  by
  ext
  simp only [mk_apply, id_coe, compr₂_apply, _root_.id, map_tmul]

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