fromSum_map_inl — Mathlib

English

The functor fromSum C D is faithful: it reflects equality of morphisms componentwise via the inclusions left and right.

Русский

Функтор fromSum C D является верным: он восстанавливает равенство морфин через включения слева и справа.

LaTeX

$$$\operatorname{fromSum} C D\;\text{ is faithful}$$$

Lean4

@[simp]
theorem fromSum_map_inl {c c' : C} (f : c ⟶ c') : (fromSum C D).map ((Sum.inl_ C D).map f) = (inclLeft C D).map f :=
  rfl

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