English
Associate to an embedding f from α to β the order embedding that maps a Finset to its image under f.
Русский
Для вложения f: α → β сопоставляется упорядоченное вложение Finset α → Finset β, которое отправляет Finset на его образ под f.
LaTeX
$$$\mathrm{mapEmbedding}(f): \mathrm{Finset}(\alpha) \hookrightarrow_{o} \mathrm{Finset}(\beta)$$$
Lean4
/-- Associate to an embedding `f` from `α` to `β` the order embedding that maps a finset to its
image under `f`. -/
def mapEmbedding (f : α ↪ β) : Finset α ↪o Finset β :=
OrderEmbedding.ofMapLEIff (map f) fun _ _ => map_subset_map