injective

Mathlib.Data.FunLike.Embedding

URI: https://scilib.ai/kg/mathlib#EmbeddingLike.injective

English

An embedding-like structure acts as an injective map on its underlying function.

Русский

Структура вида вложения эмулирует инъективное отображение на своей скрытой функции.

LaTeX

$$$\forall f:\, F, \operatorname{Injective}(f) \text{ where } f \text{ is interpreted as a function}. $$$

Lean4

protected theorem injective (f : F) : Function.Injective f :=
  injective' f

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

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

Разделы

Аффилиация

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