comp — Mathlib

English

If α: F ⟶ G and β: G ⟶ H are equifibered, then their composite α ≫ β is equifibered.

Русский

Если α: F ⟶ G и β: G ⟶ H — равнолистовые, то их композиция α ≫ β тоже равнолистовая.

LaTeX

$$Equifibered α → Equifibered β → Equifibered (α ≫ β)$$

Lean4

theorem comp {F G H : J ⥤ C} {α : F ⟶ G} {β : G ⟶ H} (hα : Equifibered α) (hβ : Equifibered β) : Equifibered (α ≫ β) :=
  fun _ _ f => (hα f).paste_vert (hβ f)

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