isLUB_iff_isGreatest — Mathlib

English

Dual to isGLB_iff_isLeast: for a nonempty Finset s in a linearly ordered type, IsLUB(s,i) holds iff i is the greatest element of s.

Русский

Двойственно isGLB_iff_isLeast: IsLUB множества эквивалентно тому, что i является наибольшим элементом s.

LaTeX

$$$ IsLUB(s,i) \\iff IsGreatest(\\langle s\\rangle,i) $$$

Lean4

theorem isLUB_iff_isGreatest [LinearOrder α] (i : α) (s : Finset α) (hs : s.Nonempty) :
    IsLUB (s : Set α) i ↔ IsGreatest (↑s) i :=
  @isGLB_iff_isLeast αᵒᵈ _ i s hs

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