symm_comp_self — Mathlib

English

For f: M ≃[L] N, the embedding associated to the inverse and the embedding associated to f compose to the identity embedding on M: f.symm.toEmbedding ∘ f.toEmbedding = Embedding.refl L M.

Русский

Для f: M ≃_L N композиция вложения обратного отображения и вложения f даёт тождественное вложение на M.

LaTeX

$$$f^{\mathrm{symm,toEmbedding}} \circ f^{\mathrm{toEmbedding}} = \mathrm{Embedding.refl}$$$

Lean4

@[simp]
theorem symm_comp_self (f : M ≃[L] N) : f.symm.comp f = refl L M := by ext;
  rw [comp_apply, symm_apply_apply, refl_apply]

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