instWeakEquivalenceI₁ — Mathlib

English

If the target category has a two-out-of-three property for weak equivalences and identities, then the right face i1 of the cylinder is a weak equivalence.

Русский

Если в категории выполняется свойство двух из трёх для слабых эквивалентностей и присутствуют единицы, то правый грань i1 цилиндра является слабой эквивалентностью.

LaTeX

$$$\text{WeakEquivalence}(P.i_1)$$$

Lean4

instance : WeakEquivalence P.i₁ :=
  weakEquivalence_of_postcomp_of_fac P.i₁_π

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