English
If i is the GLB of the set s, and s is nonempty, then i belongs to s.
Русский
Если i является наибольшим нижним пределом множества s и s непусто, то i принадлежит s.
LaTeX
$$$ IsGLB(s,i) \\land s \\neq \\varnothing \\Rightarrow i \\in s $$$
Lean4
theorem isGLB_mem [LinearOrder α] {i : α} (s : Finset α) (his : IsGLB (s : Set α) i) (hs : s.Nonempty) : i ∈ s :=
by
rw [← mem_coe]
exact ((isGLB_iff_isLeast i s hs).mp his).1