swap_map_inl — Mathlib

English

On arrows within the left summand, the swap acts as the identity: swap.map f = f for f : inl X ⟶ inl Y.

Русский

На стрелках внутри левой суммы swap действует как тождество: swap.map f = f для f : inl X ⟶ inl Y.

LaTeX

$$$ (\\mathrm{swap}\\, C\\, D).\\mathrm{map} f = f $ для $f : \\mathrm{inl}\\, X \\to \\mathrm{inl}\\, Y$$$

Lean4

@[simp]
theorem swap_map_inl {X Y : C} {f : inl X ⟶ inl Y} : (swap C D).map f = f :=
  rfl

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