id_comp — Mathlib

English

Left identity for StrictlyUnitaryLaxFunctor: id on B acts as an identity with respect to F.

Русский

Левая идентичность для StrictlyUnitaryLaxFunctor: тождественный функтор действует как идентичность.

LaTeX

$$$\forall F: StrictlyUnitaryLaxFunctor B C, (StrictlyUnitaryLaxFunctor.id B).comp F = F$$$

Lean4

/-- Composition of `StrictlyUnitaryLaxFunctor` is strictly left unitary -/
theorem id_comp (F : StrictlyUnitaryLaxFunctor B C) : (StrictlyUnitaryLaxFunctor.id B).comp F = F :=
  by
  ext
  · simp
  all_goals
    · rw [heq_iff_eq]
      ext
      simp

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