out_inj

Mathlib.Data.Erased

URI: https://scilib.ai/kg/mathlib#Erased.out_inj

English

If a.out = b.out for erased elements a,b, then a = b; the out map is injective on Erased α.

Русский

Если a.out = b.out для стертых элементов a,b, то a = b; отображение out инъективно на Erased α.

LaTeX

$$$a.\\mathrm{out} = b.\\mathrm{out} \\Rightarrow a = b$$$

Lean4

@[ext]
theorem out_inj {α} (a b : Erased α) (h : a.out = b.out) : a = b := by simpa using congr_arg mk h

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

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

Разделы

Аффилиация

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