coeEmbedding

Mathlib.Logic.Embedding.Basic

URI: https://scilib.ai/kg/mathlib#Equiv.coeEmbedding

English

There is a canonical coercion from Equiv α β to Embedding α β, via toEmbedding.

Русский

Существует каноническое приведение из Equiv α β к Embedding α β через toEmbedding.

LaTeX

$$$\text{coeEmbedding} : (\alpha \simeq \beta) \to (\alpha \hookrightarrow \beta)$$$

Lean4

instance coeEmbedding : Coe (α ≃ β) (α ↪ β) :=
  ⟨Equiv.toEmbedding⟩

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

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

Разделы

Аффилиация

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