boundedOrder — Mathlib

English

Under the hypotheses HasInitial, InitialMonoClass, Subobject B inherits a lattice structure; in particular Subobject B is a bounded order.

Русский

При допущениях HasInitial, InitialMonoClass подмножество подпредметов B образует упорядоченное множество с верхней и нижней границами.

LaTeX

$$$\text{BoundedOrder}(\mathrm{Subobject}\, B)$$$

Lean4

instance boundedOrder [HasInitial C] [InitialMonoClass C] {B : C} : BoundedOrder (Subobject B) :=
  { Subobject.orderTop, Subobject.orderBot with }

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