map_monotone — Mathlib

English

Let R and S be presieves on an object X in a category, with R contained in S (R ≤ S). Then for every functor F, the image of R under F is contained in the image of S under F; i.e., R.map F ≤ S.map F.

Русский

Пусть R и S — пресейвы на объекте X в категории, причём R ⊆ S. Тогда для любого функторa F образ R по F содержит образ S по F; т.е. R.map F ⊆ S.map F.

LaTeX

$$$R \\le S \\Rightarrow R.map F \\le S.map F$$$

Lean4

theorem map_monotone {R S : Presieve X} (h : R ≤ S) : R.map F ≤ S.map F := fun _ _ ⟨hf⟩ ↦ ⟨h _ hf⟩

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