coe_injective

Mathlib.Topology.LocallyConstant.Basic

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

English

The coercion map LocallyConstant X Y → (X → Y) is injective.

Русский

Коэрция LocallyConstant X Y → (X → Y) инъективна.

LaTeX

$$LocallyConstant.coe_injective$$

Lean4

theorem coe_injective : @Function.Injective (LocallyConstant X Y) (X → Y) (↑) := fun _ _ => DFunLike.ext'

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

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

Разделы

Аффилиация

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