mapEmbedding — Mathlib

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

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