isGreatest_Ioc — Mathlib

English

Let a < b. The set (a,b] has b as its greatest element; i.e., b ∈ Ioc(a,b) and every element of Ioc(a,b) is ≤ b.

Русский

Пусть a < b. Множество (a,b] имеет b в качестве наибольшего элемента; то есть b ∈ Ioc(a,b) и каждый элемент Ioc(a,b) не превосходит b.

LaTeX

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

Lean4

theorem isGreatest_Ioc (h : a < b) : IsGreatest (Ioc a b) b :=
  ⟨right_mem_Ioc.2 h, fun _ => And.right⟩

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