max_mem_image_coe — Mathlib

English

Let s be a nonempty finite subset of a linear order α. Then the maximum of s, viewed in WithBot α, lies in the image of s under the embedding ↑: α → WithBot α.

Русский

Пусть s — непустое конечноe подмножество линейного порядка α. Тогда максимум s, рассматриваемый как элемент WithBot α, принадлежит образу s через отображение ↑: α → WithBot α.

LaTeX

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

Lean4

theorem max_mem_image_coe {s : Finset α} (hs : s.Nonempty) : s.max ∈ (s.image (↑) : Finset (WithBot α)) :=
  mem_image.2 ⟨max' s hs, max'_mem _ _, coe_max' hs⟩

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