exists_next_right — Mathlib

English

In a finite linearly ordered set, if there is an element of s strictly greater than x, there is a least such element; it is the next right element after x in s.

Русский

Для конечного линейно упорядоченного множества, если существует элемент s, больший x, то существует наименьший из таких элементов; он есть следующий справа элемент после x в s.

LaTeX

$$$\\exists y\\in s\\; (x

Lean4

theorem exists_next_right {x : α} {s : Finset α} (h : ∃ y ∈ s, x < y) : ∃ y ∈ s, x < y ∧ ∀ z ∈ s, x < z → y ≤ z :=
  have Hne : (s.filter (x < ·)).Nonempty := h.imp fun y hy => mem_filter.2 (by simpa)
  have aux := mem_filter.1 (min'_mem _ Hne)
  ⟨min' _ Hne, aux.1, by simp, fun z hzs hz => min'_le _ _ <| mem_filter.2 ⟨hzs, by simpa⟩⟩

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