isLeast_Ico — Mathlib

English

Let a < b. The interval [a,b) has a as its least element; i.e., a ∈ Ico(a,b) and ∀ x ∈ Ico(a,b), a ≤ x.

Русский

Пусть a < b. Промежуток [a,b) имеет a в качестве наименьшего элемента; то есть a ∈ Ico(a,b) и для всех x ∈ Ico(a,b) выполняется a ≤ x.

LaTeX

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

Lean4

theorem isLeast_Ico (h : a < b) : IsLeast (Ico a b) a :=
  ⟨left_mem_Ico.2 h, fun _ => And.left⟩

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