coe_eq_of_eq_mk — Mathlib

English

If a is a member of a subtype and its underlying value equals b, then a equals the pair ⟨b, h▸a.2⟩, i.e., a is determined by its value.

Русский

Если a принадлежит подтипy и его основанное значение равно b, то a = ⟨b, h ▸ a.2⟩, то есть a определяется значением.

LaTeX

$$$\forall a:{a\; //\; p a}\, {b:\alpha}\; (h: a.1 = b)\;:\; a = \langle b, h \;\text{▸} \; a.2 \rangle$$$

Lean4

theorem coe_eq_of_eq_mk {a : { a // p a }} {b : α} (h : ↑a = b) : a = ⟨b, h ▸ a.2⟩ :=
  Subtype.ext h

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