iInf_obj — Mathlib

English

For a family of subpresheaves (S i), the object of their infimum at U is the intersection over i of the objects (S i).obj U.

Русский

Для семейства подпрешафов (S i) объект их инфимума в U равен пересечению по i объектов (S_i).obj U.

LaTeX

$$$\\left( \\bigwedge_i S_i \\right).obj U = \\bigcap_i (S_i).obj U$$$

Lean4

@[simp]
theorem iInf_obj {ι : Type*} (S : ι → Subpresheaf F) (U : Cᵒᵖ) : (⨅ i, S i).obj U = ⋂ i, (S i).obj U := by
  simp [iInf, sInf_obj]

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