coe_inj

Mathlib.Data.Subtype

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

English

For any a,b in Subtype p, a.α = b.α iff a = b; i.e., equality of underlying elements iff equality of subtypes.

Русский

Для любых a,b ∈ Subtype p, (a : α) = (b : α) тогда и только тогда, когда a = b.

LaTeX

$$$\forall a,b : Subtype\, p,\ (a : \alpha) = (b : \alpha) \iff a = b.$$$

Lean4

theorem coe_inj {a b : Subtype p} : (a : α) = b ↔ a = b :=
  coe_injective.eq_iff

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

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

Разделы

Аффилиация

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