embeddingLike

Mathlib.ModelTheory.ElementaryMaps

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.ElementaryEmbedding.embeddingLike

English

An elementary embedding carries the structure of an embedding, hence is EmbeddingLike.

Русский

Элементарное вложение имеет структуру отображения-названно как EmbeddingLike.

LaTeX

$$$\text{EmbeddingLike} (M \hookrightarrow_L N)\; M\; N$$$

Lean4

instance embeddingLike : EmbeddingLike (M ↪ₑ[L] N) M N :=
  { show FunLike (M ↪ₑ[L] N) M N from inferInstance with injective' := injective }

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru