English
Let A be a finite set of elements of α. Create a finite set of elements of Option α by tagging each element with the constructor some and by including the distinguished element none. This construction defines an order-preserving embedding from Finset α into Finset (Option α), sending s to {none} ∪ {some a : a ∈ s}.
Русский
Пусть A — конечное множество элементов α. Получим конечное множество элементов Option α, пометив каждый элемент конструктором some и добавив особый элемент none. Эта конструкция задаёт порядок-встраивание от Finset α в Finset (Option α), отображая s на {none} ∪ {some a : a ∈ s}.
LaTeX
$$$insertNone(s) = \\{\\text{none}\\} \\cup \\{\\text{some}(a) \\mid a \\in s\\}$ и $insertNone : \\mathrm{Finset}\\,\\alpha \\hookrightarrow\\mathrm{Finset}(\\mathrm{Option}\\,\\alpha)$ является ордер-встраиванием.$$
Lean4
/-- Given a finset on `α`, lift it to being a finset on `Option α`
using `Option.some` and then insert `Option.none`. -/
def insertNone : Finset α ↪o Finset (Option α) :=
(OrderEmbedding.ofMapLEIff fun s => cons none (s.map Embedding.some) <| by simp) fun s t => by
rw [le_iff_subset, cons_subset_cons, map_subset_map, le_iff_subset]
