instIsEquivalenceLeftExtensionCompPrecomp

English

The existence of a left extension along L' after postcomposition by G is equivalent to the existence along L; this is expressed by an equivalence of categories between the relevant structured arrows.

Русский

Существование левого расширения вдоль L' после посткомпозиции по G эквивалентно существованию вдоль L; это выражается эквивалентностью структурированных стрелок.

LaTeX

$$ex.IsEquivalence$$

Lean4

noncomputable instance : IsEquivalence (LeftExtension.precomp L F G) := by apply StructuredArrow.isEquivalenceMap₂

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