bounded_gt_Icc — Mathlib

English

For all a, b, the closed interval Icc(a,b) is bounded below with respect to >; lower bound by a (exists due to NoMinOrder).

Русский

Для всех a, b замкнутый интервал Icc(a,b) ограничен снизу относительно >; нижняя граница — a (существует из NoMinOrder).

LaTeX

$$$\forall a,b:\ Bound\ (>)(Icc\ a\ b)$$$

Lean4

theorem bounded_gt_Icc [Preorder α] [NoMinOrder α] (a b : α) : Bounded (· > ·) (Icc a b) :=
  (bounded_gt_Ici a).mono Set.Icc_subset_Ici_self

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