map_functorPullback — Mathlib

English

The pushforward of the functorPullback by F is contained in the original presieve R; i.e., R.functorPullback F).map F ≤ R.

Русский

Перемещение через F вытянутого конструктора (functorPullback) содержится в исходной предсистеме R.

LaTeX

$$$R.functorPullback(F).map F \\le R$$$

Lean4

theorem map_functorPullback {X : C} (R : Presieve (F.obj X)) : (R.functorPullback F).map F ≤ R := fun _ _ ⟨hu⟩ ↦ hu

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