imageMonoIsoSource_inv_ι — Mathlib

English

If f: X → Y is a monomorphism, then the canonical isomorphism between X and the image of f has inverse inv, and inv; image inclusions satisfy inv ≫ image.ι_f = f.

Русский

Пусть f: X → Y моно, тогда существует канонический изоморфизм между X и образом f; его обратная стрелка и включение образа в Y удовлетворяют inv ≫ image.ι_f = f.

LaTeX

$$$ (\\mathrm{imageMonoIsoSource}(f))^{-1} \\circ \\mathrm{image}.\\iota(f) = f $$$

Lean4

@[reassoc (attr := simp)]
theorem imageMonoIsoSource_inv_ι [Mono f] : (imageMonoIsoSource f).inv ≫ image.ι f = f := by simp [imageMonoIsoSource]

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