English
If two arrows f0,f1:X→Y are left-homotopic along a cylinder P, then they have the same weak equivalence status; i.e., f0 is a weak equivalence iff f1 is a weak equivalence.
Русский
Если стрелки f0 и f1:X→Y однолинейно гомотопичны по цилиндру P, то они имеют одинаковый статус слабой эквивалентности; тождественно f0 является слабой эквивалентностью тогда и только тогда, когда f1 является слабой эквивалентностью.
LaTeX
$$$\forall P\, (P.LeftHomotopy\ f0\ f1) \Rightarrow (\mathrm{WeakEquivalence}(f0) \iff \mathrm{WeakEquivalence}(f1))$$$
Lean4
theorem weakEquivalence_iff [(weakEquivalences C).HasTwoOutOfThreeProperty] [(weakEquivalences C).ContainsIdentities]
{f₀ f₁ : X ⟶ Y} (h : P.LeftHomotopy f₀ f₁) : WeakEquivalence f₀ ↔ WeakEquivalence f₁ :=
by
revert P f₀ f₁
suffices ∀ (P : Cylinder X) {f₀ f₁ : X ⟶ Y} (h : P.LeftHomotopy f₀ f₁), WeakEquivalence f₀ → WeakEquivalence f₁ from
fun _ _ _ h ↦ ⟨this _ h, this _ h.symm⟩
intro P f₀ f₁ h h₀
have := weakEquivalence_of_precomp_of_fac h.h₀
rw [← h.h₁]
infer_instance
