of_comp_right — Mathlib

English

If ψ is a covering prefunctor and the composite φ ⋙q ψ is covering, then φ is a covering prefunctor.

Русский

Если ψ — покрывающий префунктор и композиция φ ⋙q ψ является покрывающим, то φ — покрывающий префунктор.

LaTeX

$$\operatorname{IsCovering}(\psi) \land \operatorname{IsCovering}(\phi \circ \psi) \Rightarrow \operatorname{IsCovering}(\phi)$$

Lean4

theorem of_comp_right (hψ : ψ.IsCovering) (hφψ : (φ ⋙q ψ).IsCovering) : φ.IsCovering :=
  ⟨fun _ => (Bijective.of_comp_iff' (hψ.star_bijective _) _).mp (hφψ.star_bijective _), fun _ =>
    (Bijective.of_comp_iff' (hψ.costar_bijective _) _).mp (hφψ.costar_bijective _)⟩

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