min_mem_image_coe — Mathlib

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⟩

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