instBoundedOrderElemOfFactLe — Mathlib

English

If a ≤ b, the interval Icc(a,b) forms a bounded order, i.e., it has both a bottom and a top element.

Русский

При a ≤ b интервал Icc(a,b) образует ограниченный порядок, у него есть и нижняя и верхняя грани.

LaTeX

$$$\text{Icc}(a,b) \text{ is a bounded order (has bottom } a \text{ and top } b).$$$

Lean4

/-- `Icc a b` is a `BoundedOrder` whenever `a ≤ b`. -/
instance [Preorder α] [Fact (a ≤ b)] : BoundedOrder (Icc a b) where

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