toEmbeddingLike

Mathlib.Data.FunLike.Equiv

URI: https://scilib.ai/kg/mathlib#EquivLike.toEmbeddingLike

English

Every EquivLike object induces an EmbeddingLike structure.

Русский

Каждый объект EquivLike определяет структуру EmbeddingLike.

LaTeX

$$$\forall E,\ EmbeddingLike E \alpha \beta$$$

Lean4

instance (priority := 100) toEmbeddingLike : EmbeddingLike E α β where injective' e := (left_inv e).injective

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

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

Разделы

Аффилиация

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