trans_toEmbedding — Mathlib

English

The embedding of a composition equals the composition of embeddings: (e trans f).toEmbedding = e.toEmbedding trans f.toEmbedding.

Русский

Вложение композиции равно композиции вложений: (e.trans f).toEmbedding = e.toEmbedding.trans f.toEmbedding.

LaTeX

$$$(e.\\mathrm{trans} f).\\mathrm{toEmbedding} = e.\\mathrm{toEmbedding}.trans f.\\mathrm{toEmbedding}$$$

Lean4

@[simp]
theorem trans_toEmbedding {α β γ : Type*} (e : α ≃ β) (f : β ≃ γ) :
    (e.trans f).toEmbedding = e.toEmbedding.trans f.toEmbedding :=
  rfl

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