English
For a nonempty Finset s in a linearly ordered type, the greatest lower bound of s equals i if and only if i is the least element of s.
Русский
Для непустого Finset в линейном порядке наибоящая нижняя граница множества совпадает с наименьшим элементом, если и только если i является минимальным элементом s.
LaTeX
$$$ IsGLB(s,i) \\iff IsLeast(\\langle s\\rangle,i) $$$
Lean4
theorem isGLB_iff_isLeast [LinearOrder α] (i : α) (s : Finset α) (hs : s.Nonempty) :
IsGLB (s : Set α) i ↔ IsLeast (↑s) i :=
by
refine ⟨fun his => ?_, IsLeast.isGLB⟩
suffices i = min' s hs by
rw [this]
exact isLeast_min' s hs
rw [IsGLB, IsGreatest, mem_lowerBounds, mem_upperBounds] at his
exact le_antisymm (his.1 (Finset.min' s hs) (Finset.min'_mem s hs)) (his.2 _ (Finset.min'_le s))
