weakEquivalence_postcomp_iff — Mathlib

English

If HasTwoOutOfThreeProperty holds for WeakEquivalences, then f is a weak equivalence whenever f ≫ g and g is a weak equivalence; and conversely.

Русский

Если справедливо свойство HasTwoOutOfThreeProperty для слабых эквивалентностей, то f — слабая эквивалентность, когда f ≫ g — слабая эквивалентность и g — слабая эквивалентность; и наоборот.

LaTeX

$$$\operatorname{WeakEquivalence}(f) \iff \operatorname{WeakEquivalence}(f\circ g)$$$

Lean4

theorem weakEquivalence_postcomp_iff [WeakEquivalence g] : WeakEquivalence (f ≫ g) ↔ WeakEquivalence f :=
  ⟨fun _ ↦ weakEquivalence_of_postcomp f g, fun _ ↦ inferInstance⟩

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