isLeast_csInf — Mathlib

English

For a nonempty set s in a ConditionallyCompleteLinearOrder, sInf s is the least element of s under ≤.

Русский

Для непустого множества s в линейном порядке с условной полнотой inf s является наименьшим элементом множества s по отношению ≤.

LaTeX

$$$ (hs : s.Nonempty) : IsLeast s (sInf s) $$$

Lean4

theorem isLeast_csInf (hs : s.Nonempty) : IsLeast s (sInf s) :=
  by
  rw [sInf_eq_argmin_on hs]
  exact ⟨argminOn_mem _ _ _, fun a ha => argminOn_le id _ ha⟩

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