bounded_gt_Ico — Mathlib

English

For all a, b, the half-open interval Ico(a,b) is bounded below with respect to >; lower bound by a.

Русский

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

LaTeX

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

Lean4

theorem bounded_gt_Ico [Preorder α] [NoMinOrder α] (a b : α) : Bounded (· > ·) (Ico a b) :=
  (bounded_gt_Ici a).mono Set.Ico_subset_Ici_self

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