inv_comp_image_ι_map — Mathlib

English

For preserves-image data, the inverse of the image map composed with mapping equals the mapped image map.

Русский

Для сохранения отображения образа обратная карта образа, взятая после отображения, совпадает с отображением образа после отображения.

LaTeX

$$$(\\mathrm{iso}\\;L\\;f)^{-1} \\circ L\\big(\\mathrm{image.\\,ι} f\\big) = L\\big(\\mathrm{image.\\,ι} f\\big) \\quad$ (schematic).$$

Lean4

@[reassoc]
theorem inv_comp_image_ι_map {X Y : A} (f : X ⟶ Y) : (iso L f).inv ≫ image.ι (L.map f) = L.map (image.ι f) := by simp

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