mapEmbedding — Mathlib

English

There is an order-embedding that sends a multiset to its image under a given embedding f.

Русский

Существует отображение с сохранением порядка, отправляющее мультисет в образ под вложение f.

LaTeX

$$$ mapEmbedding (f) : Multiset \\alpha \\hookrightarrowo Multiset \\beta $$$

Lean4

/-- Associate to an embedding `f` from `α` to `β` the order embedding that maps a multiset to its
image under `f`. -/
@[simps!]
def mapEmbedding (f : α ↪ β) : Multiset α ↪o Multiset β :=
  OrderEmbedding.ofMapLEIff (map f) fun _ _ => map_le_map_iff f.inj'

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