self_comp_symm_toEmbedding — Mathlib

English

If two L-equivalences f and g agree on every input x ∈ M, then f = g.

Русский

Если две L-эквивалентности f и g совпадают на каждом входе x ∈ M, то f = g.

LaTeX

$$$\forall f,g : M \cong_L N,\ (\forall x\in M, f(x)=g(x)) \Rightarrow f=g$$$

Lean4

@[simp]
theorem self_comp_symm_toEmbedding (f : M ≃[L] N) : f.toEmbedding.comp f.symm.toEmbedding = Embedding.refl L N := by
  rw [← comp_toEmbedding, self_comp_symm, refl_toEmbedding]

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