comp — Mathlib

English

If φ : U ⇢ V and ψ : V ⇢ W are covering prefuntors, then their composition φ ⋙q ψ is a covering prefunctor from U to W.

Русский

Если φ : U ⥤q V и ψ : V ⥤q W являются покрывающими префункторы, то их композиция φ ⋙q ψ является покрывающим префунктором от U к W.

LaTeX

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

Lean4

theorem comp (hφ : φ.IsCovering) (hψ : ψ.IsCovering) : (φ ⋙q ψ).IsCovering :=
  ⟨fun _ => (hψ.star_bijective _).comp (hφ.star_bijective _), fun _ =>
    (hψ.costar_bijective _).comp (hφ.costar_bijective _)⟩

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