exists_eq_subtype_mk_iff — Mathlib

English

A simp lemma: an element a of Subtype p can be written as Subtype.mk b h iff the underlying value equals b.

Русский

Лемма-упрощение: элемент a подтипа p выражается как Subtype.mk b h тогда, когда базовое значение равно b.

LaTeX

$$$@[simp]\ theorems\ (\exists h : p\, b,\ a = Subtype.mk b h) \iff \uparrow a = b$$$

Lean4

@[simp]
theorem _root_.exists_eq_subtype_mk_iff {a : Subtype p} {b : α} : (∃ h : p b, a = Subtype.mk b h) ↔ ↑a = b :=
  coe_eq_iff.symm

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