max_mem_insert_bot_image_coe — Mathlib

English

For any Finset s of α, the maximum element of s, considered in WithBot α, belongs to the Finset obtained by inserting ⊥ into the image of s under the embedding ↑.

Русский

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

LaTeX

$$$ s.max \\in (insert \\bot (s.image (\\uparrow)) : Finset (WithBot \\ α)) $$$

Lean4

theorem max_mem_insert_bot_image_coe (s : Finset α) : s.max ∈ (insert ⊥ (s.image (↑)) : Finset (WithBot α)) :=
  mem_insert.2 <| s.eq_empty_or_nonempty.imp max_eq_bot.2 max_mem_image_coe

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