sSup_obj — Mathlib

English

Let S be a set of subpresheaves of F. The objectwise supremum captures, at each index, the supremum of the corresponding sets of sections.

Русский

Пусть S — множество подпрешафов F. На каждом индексе равенствy supremum по соответствующим множествам секций.

LaTeX

$$$\\left( \\mathrm{sSup} S \\right).obj U = \\mathrm{sSup} (\\mathrm{Set.image} (\\lambda T. T.obj U)\\, S)$$$

Lean4

theorem sSup_obj (S : Set (Subpresheaf F)) (U : Cᵒᵖ) : (sSup S).obj U = sSup (Set.image (fun T ↦ T.obj U) S) :=
  rfl

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