homOfLe — Mathlib

English

As above, the object of the infimum of a family at U is the intersection of their objects at U.

Русский

Как выше, объект инфимума семейства в U равен пересечению их объектов в U.

LaTeX

$$$\\left( \\mathrm{iInf} \\; S \\right).obj U = \\bigcap_i (S_i).obj U$$$

Lean4

/-- The inclusion of a subpresheaf to a larger subpresheaf -/
@[simps]
def homOfLe {G G' : Subpresheaf F} (h : G ≤ G') : G.toPresheaf ⟶ G'.toPresheaf where app U x := ⟨x, h U x.prop⟩

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