exists_next_left — Mathlib

English

Dual statement: in a finite linearly ordered set, if there exists y ∈ s with y < x, there is a least such element on the left; i.e., the next left element after x in s.

Русский

Двойственное утверждение: в конечном линейно упорядоченном множестве, если существует y ∈ s с y < x, существует наименьшее такое y слева; то есть предшествующий элемент слева от x в s.

LaTeX

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

Lean4

theorem exists_next_left {x : α} {s : Finset α} (h : ∃ y ∈ s, y < x) : ∃ y ∈ s, y < x ∧ ∀ z ∈ s, z < x → z ≤ y :=
  @exists_next_right αᵒᵈ _ x s h

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