instOrderBotElemOfFactLe — Mathlib

English

For a preorder α and a ≤ b, Icc(a,b) has a bottom element, namely a, making it an OrderBot when a ≤ b holds (as a fact).

Русский

При предордере α и условии a ≤ b, у интервала Icc(a,b) есть наименьший элемент, равный a.

LaTeX

$$$\text{If } [\text{Preorder } \alpha] \text{ and } a \le b, \text{ then } a \text{ is the bottom of } \mathrm{Icc}(a,b).$$$

Lean4

/-- `Icc a b` has a bottom element whenever `a ≤ b`. -/
instance [Preorder α] [Fact (a ≤ b)] : OrderBot (Icc a b) :=
  (isLeast_Icc Fact.out).orderBot

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