orderBot — Mathlib

English

There is a bottom element in the subobject lattice of any object X, which is below every subobject of X.

Русский

В решетке подобъектов любого объекта X существует минимальный элемент, который лежит ниже любого подобъекта X.

LaTeX

$$$ \\forall S \\in \\mathrm{Sub}(X), \\bot \\le S $$$

Lean4

instance orderBot {X : C} : OrderBot (Subobject X)
    where
  bot := Quotient.mk'' ⊥
  bot_le := by
    refine Quotient.ind' fun f => ?_
    exact ⟨MonoOver.botLE f⟩

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