swapCompInl — Mathlib

English

Precomposing swap with the left inclusion yields the right inclusion as an iso.

Русский

Предпоставление swap по левой инклюзии даёт правую инклюзию как изоморфизм.

LaTeX

$$$ (inl_ C D) \\circ (swap C D) \\cong inr_ D C $$$

Lean4

/-- Precomposing `swap` with the left inclusion gives the right inclusion. -/
@[simps! hom_app inv_app]
def swapCompInl : inl_ C D ⋙ swap C D ≅ inr_ D C :=
  Functor.inlCompSum' (inr_ _ _) (inl_ _ _)

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