coe_min' — Mathlib

English

For a nonempty finite subset s of a linearly ordered set α, the minimum element obtained via the min' construction equals the Finset's minimum element, i.e., the two notions of minimum agree.

Русский

Для непустого конечного подмножества s линейно упорядоченного множества α минимальный элемент, полученный через конструкцию min', совпадает с минимальным элементом Finset.

LaTeX

$$$ (s.min'\\, hs) = s.min $$$

Lean4

theorem coe_min' {s : Finset α} (hs : s.Nonempty) : ↑(s.min' hs) = s.min :=
  coe_inf' hs id

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