isGLB_inf' — Mathlib

English

For any nonempty finite subset s of α, the infimum inf' s H id is the greatest lower bound of s.

Русский

Для непустого конечного подмножества s ⊆ α инф'_inf' s является наибольшей нижней границей множества s.

LaTeX

$$IsGLB(s, inf' s H id)$$

Lean4

theorem isGLB_inf' {s : Finset α} (hs : s.Nonempty) : IsGLB s (inf' s hs id) :=
  ⟨fun x h => id_eq x ▸ inf'_le id h, fun _ h => Finset.le_inf' hs id h⟩

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