English
There exists an order-embedding that lifts finite subsets of α to Finset (WithBot α) by inserting a bottom element.
Русский
Существует отображение вложения по порядку, переводя конечные подмножества α в Finset WithBot α через вставку нижней границы.
LaTeX
$$$ insertBot : Finset\,\alpha \hookrightarrow_o Finset\,(WithBot\,\alpha) $$$
Lean4
/-- Given a finset on `α`, lift it to being a finset on `WithBot α`
using `WithBot.some` and then insert `⊥`. -/
def insertBot : Finset α ↪o Finset (WithBot α) :=
OrderEmbedding.ofMapLEIff (fun s => cons ⊥ (s.map Embedding.coeWithBot) <| by simp)
(fun s t => by rw [le_iff_subset, cons_subset_cons, map_subset_map, le_iff_subset])
