isGLB_mem — Mathlib

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

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