comp — Mathlib

English

The composition of two cover-preserving functors is cover-preserving.

Русский

Состав двух покрывающих покрытие функторов сохраняет покрытие.

LaTeX

$$$[F: J \\to K] \\land [G: K \\to L] \\Rightarrow (F \\circ G): J \\to L$$$

Lean4

/-- The composition of two cover-preserving functors is cover-preserving. -/
theorem comp {F} (hF : CoverPreserving J K F) {G} (hG : CoverPreserving K L G) : CoverPreserving J L (F ⋙ G) :=
  ⟨fun hS => by
    rw [Sieve.functorPushforward_comp]
    exact hG.cover_preserve (hF.cover_preserve hS)⟩

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