val_inj

Mathlib.Data.Subtype

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

English

Equality of the underlying values implies equality of subtypes; i.e., a.val = b.val ↔ a = b.

Русский

Равенство базовых значений эквивалентно равенству подтипов; a.val = b.val ↔ a = b.

LaTeX

$$$\forall a,b : Subtype\, p,\ a.\mathrm{val} = b.\mathrm{val} \iff a = b.$$$

Lean4

theorem val_inj {a b : Subtype p} : a.val = b.val ↔ a = b :=
  coe_inj

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

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

Разделы

Аффилиация

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