sInf_obj — Mathlib

English

Let S be a set of subpresheaves of F. The objectwise infimum is given by the infimum of the corresponding sets at each index.

Русский

Пусть S — множество подпрешафов F. Обратная инфимум по каждому индексу равен инфимуму соответствующих множеств.

LaTeX

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

Lean4

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

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