English
Let s be a nonempty finite subset of a linear order α. Then the minimum of s, viewed in WithTop α, lies in the image of s under the embedding ↑: α → WithTop α.
Русский
Пусть s — непустое конечное подмножество линейного порядка α. Тогда минимум s, рассматриваемый как элемент WithTop α, принадлежит образу s через отображение ↑: α → WithTop α.
LaTeX
$$$ s.min \\in (s.image (\\uparrow) : Finset (WithTop \\ α)) $$$
Lean4
theorem min_mem_image_coe {s : Finset α} (hs : s.Nonempty) : s.min ∈ (s.image (↑) : Finset (WithTop α)) :=
mem_image.2 ⟨min' s hs, min'_mem _ _, coe_min' hs⟩