bounded_ge_Ioc — Mathlib

English

Let α be a preorder and a, b ∈ α. Then the interval Ioc(a, b) is bounded below with respect to the order ≤; equivalently, there exists m ∈ α such that for all x ∈ Ioc(a, b) we have m ≤ x.

Русский

Пусть α — предпорядок и а, b ∈ α. Тогда интервал Ioc(a, b) ограничен снизу по отношению к порядку ≤; существует m ∈ α такой, что для всех x ∈ Ioc(a, b) выполняется m ≤ x.

LaTeX

$$$$\forall a,b \in \alpha,\ \exists m \in \alpha,\ \forall x \in Ioc(a,b),\ m \le x.$$$$

Lean4

theorem bounded_ge_Ioc [Preorder α] (a b : α) : Bounded (· ≥ ·) (Ioc a b) :=
  (bounded_ge_Ioi a).mono Set.Ioc_subset_Ioi_self

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