instMonoFunctorOppositeTypeι — Mathlib

English

As above, the object of the supremum of a family of subpresheaves at U is the union of their objects at U.

Русский

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

LaTeX

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

Lean4

instance : Mono G.ι :=
  ⟨@fun _ _ _ e => NatTrans.ext <| funext fun U => funext fun x => Subtype.ext <| congr_fun (congr_app e U) x⟩

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