middle_spec — Mathlib

English

The composition of the middle and its companion equals the original arrow f: I.toMiddleHom ≫ I.fromMiddleHom = I.f.

Русский

Композицiя середины и её пары равна исходной стрелке f: I.toMiddleHom ≫ I.fromMiddleHom = I.f.

LaTeX

$$$I.toMiddleHom \circ I.fromMiddleHom = I.f$$$

Lean4

theorem middle_spec {X : C} {S : J.Cover X} {T : ∀ I : S.Arrow, J.Cover I.Y} (I : (S.bind T).Arrow) :
    I.toMiddleHom ≫ I.fromMiddleHom = I.f :=
  I.hf.choose_spec.choose_spec.choose_spec.choose_spec.2

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