isLeast_Icc — Mathlib

English

Let a ≤ b. The closed interval [a,b] has a as its least element; i.e., a is the smallest element of [a,b].

Русский

Пусть a ≤ b. Замкнутый интервал [a,b] имеет a в качестве наименьшего элемента; то есть a является наименьшим элементом внутри [a,b].

LaTeX

$$$a \le b \implies (a \in \mathrm{Icc}(a,b) \wedge \forall x \in \mathrm{Icc}(a,b), a \le x).$$$

Lean4

theorem isLeast_Icc (h : a ≤ b) : IsLeast (Icc a b) a :=
  ⟨left_mem_Icc.2 h, fun _ => And.left⟩

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