bounded_ge_Icc — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem bounded_ge_Icc [Preorder α] (a b : α) : Bounded (· ≥ ·) (Icc a b) :=
  (bounded_ge_Ici a).mono Set.Icc_subset_Ici_self

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