weakEquivalence_of_postcomp — Mathlib

English

If g is a weak equivalence and f ≫ g is a weak equivalence, then f is a weak equivalence.

Русский

Если g — слабая эквивалентность, и f ≫ g — слабая эквивалентность, то f — слабая эквивалентность.

LaTeX

$$$\text{WeakEquivalence}(f) \;\text{if } \text{WeakEquivalence}(g) \text{ and } \text{WeakEquivalence}(f\circ g)$$$

Lean4

theorem weakEquivalence_of_postcomp [hg : WeakEquivalence g] [hfg : WeakEquivalence (f ≫ g)] : WeakEquivalence f :=
  by
  rw [weakEquivalence_iff] at hg hfg ⊢
  exact of_postcomp _ _ _ hg hfg

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