bounded_ge_Ico — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem bounded_ge_Ico [Preorder α] (a b : α) : Bounded (· ≥ ·) (Ico a b) :=
  (bounded_ge_Ici a).mono Set.Ico_subset_Ici_self

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