equiv_symm_toEmbedding_trans_toEmbedding

English

If e: α ≃ β, then e.symm.toEmbedding ∘ e.toEmbedding = Embedding.refl α.

Русский

Если e: α ≃ β, то e.symm.toEmbedding ∘ e.toEmbedding = Embedding.refl α.

LaTeX

$$$e : \\alpha \\simeq \\beta\\;\\Rightarrow\\; e^{\\text{symm toEmbedding}} \\circ e^{\\text{toEmbedding}} = \\mathrm{refl}_{\\alpha}$$$

Lean4

@[simp]
theorem equiv_symm_toEmbedding_trans_toEmbedding {α β : Sort*} (e : α ≃ β) :
    e.symm.toEmbedding.trans e.toEmbedding = Embedding.refl _ :=
  by
  ext
  simp

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