toEmbedding_coeEquiv_trans — Mathlib

English

The embedding arising from the equivalence coeEquiv is compatible with the subtype embedding, i.e., the two ways of embedding coincide.

Русский

Встройка, полученная из эквивалентности coeEquiv, совместима со встроекой подтипов; два способа вложения совпадают.

LaTeX

$$m.coeEquiv.toEmbedding.trans (Function.Embedding.subtype _) = m.coeEmbedding$$

Lean4

@[simp]
theorem toEmbedding_coeEquiv_trans (m : Multiset α) :
    m.coeEquiv.toEmbedding.trans (Function.Embedding.subtype _) = m.coeEmbedding := by ext <;> rfl

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