injective_toEmbedding — Mathlib

English

Injectivity of the map from L-equivalences to embeddings: if toEmbedding f = toEmbedding g then f = g.

Русский

Инъективность отображения из эквивалентностей L в вложения: если toEmbedding f = toEmbedding g, то f = g.

LaTeX

$$$\forall f,g:\ M \simeq_L N,\; (toEmbedding\; f = toEmbedding\; g) \Rightarrow f = g.$$$

Lean4

theorem injective_toEmbedding : Function.Injective (toEmbedding : (M ≃[L] N) → M ↪[L] N) := by intro _ _ h;
  apply DFunLike.coe_injective; exact congr_arg (DFunLike.coe ∘ Embedding.toHom) h

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