coe_injective

Mathlib.Data.FunLike.Basic

URI: https://scilib.ai/kg/mathlib#DFunLike.coe_injective

English

The coercion map from a function-like object F to its underlying function is injective.

Русский

Коэрцирование из объектов типа F к их базовой функции инъективно.

LaTeX

$$$\operatorname{Injective}(\mathrm{coe}: F \to \prod_{a:\alpha} \beta(a)).$$$

Lean4

theorem coe_injective : Function.Injective (fun f : F ↦ (f : ∀ a : α, β a)) :=
  DFunLike.coe_injective'

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

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

Разделы

Аффилиация

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