sInf — Mathlib

English

Under the assumptions, the infimum sInf(s) of a set of subobjects s is defined as the Subobject generated by the widePullbackι map.

Русский

При данных допущениях infimum sInf(s) множества подпредметов s определяется как подпредмет, порожденный отображением widePullbackι.

LaTeX

$$def sInf {A : C} (s : Set (Subobject A)) : Subobject A := Subobject.mk (widePullbackι s)$$

Lean4

/-- When `[WellPowered C]` and `[HasWidePullbacks C]`, `Subobject A` has arbitrary infimums.
-/
def sInf {A : C} (s : Set (Subobject A)) : Subobject A :=
  Subobject.mk (widePullbackι s)

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