instCompleteLinearOrderElemIccOfFactLe

English

If t is not bounded below, then sInf t equals the default.

Русский

Если t не ограничено снизу, то инфиминум t равен дефолтному.

LaTeX

$$$$ \neg \operatorname{BddBelow}(t) \Rightarrow \operatorname{sInf}(t) = \text{default}. $$$$

Lean4

/-- Complete linear order structure on `Set.Icc` -/
noncomputable instance [ConditionallyCompleteLinearOrder α] {a b : α} [Fact (a ≤ b)] :
    CompleteLinearOrder (Set.Icc a b) :=
  { Set.Icc.completeLattice, Subtype.instLinearOrder _, LinearOrder.toBiheytingAlgebra _ with }

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