isLUB_mem — Mathlib

English

If i is the LUB of the set s, and s is nonempty, then i belongs to s.

Русский

Если i является наибольшим верхним пределом множества s и s непусто, то i принадлежит s.

LaTeX

$$$ IsLUB(s,i) \\land s \\neq \\varnothing \\Rightarrow i \\in s $$$

Lean4

theorem isLUB_mem [LinearOrder α] {i : α} (s : Finset α) (his : IsLUB (s : Set α) i) (hs : s.Nonempty) : i ∈ s :=
  @isGLB_mem αᵒᵈ _ i s his hs

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