min_mem_insert_top_image_coe — Mathlib

English

For any Finset s of α, the minimum element of s, considered in WithTop α, lies in the Finset obtained by inserting ⊤ into the image of s under the embedding ↑.

Русский

Для любого Finset s в α минимум s, рассматриваемый как элемент WithTop α, принадлежит Finset, полученному добавлением ⊤ в образ s через ↑.

LaTeX

$$$ s.min \\in (insert \\top (s.image (\\uparrow)) : Finset (WithTop \\ α)) $$$

Lean4

theorem min_mem_insert_top_image_coe (s : Finset α) : s.min ∈ (insert ⊤ (s.image (↑)) : Finset (WithTop α)) :=
  mem_insert.2 <| s.eq_empty_or_nonempty.imp min_eq_top.2 min_mem_image_coe

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