coe_injective

Mathlib.Data.Subtype

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

English

The coercion map from the subtype to the ambient type is injective.

Русский

Коэрцирование подтипа в окружный тип инъективно.

LaTeX

$$$\operatorname{Injective}\big(\lambda a : \{ x // p x \}, (a : \alpha)\big)$.$$

Lean4

theorem coe_injective : Injective (fun (a : Subtype p) ↦ (a : α)) := fun _ _ ↦ Subtype.ext

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

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

Разделы

Аффилиация

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