generate_functorPullback_le — Mathlib

English

For a functor F, the generated functorPullback is contained in the functorPullback of the generated presieve: generate (R.functorPullback F) ≤ functorPullback F (generate R).

Русский

Для функторa F порожденное functorPullback вложено в functorPullback от порожденного presieve: generate (R.functorPullback F) ≤ functorPullback F (generate R).

LaTeX

$$$ \\mathrm{generate}(R.{\\text{functorPullback}} F) \\le \\mathrm{functorPullback} F(\\mathrm{generate} R) $$$

Lean4

theorem generate_functorPullback_le {X : C} (R : Presieve (F.obj X)) :
    generate (R.functorPullback F) ≤ functorPullback F (generate R) :=
  by
  rw [generate_le_iff]
  intro Z g hg
  exact le_generate _ _ hg

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