exists_subtype_mk_eq_iff — Mathlib

English

A simp lemma: there exists h with a = Subtype.mk b h iff b = a.

Русский

Лемма-упрощение: существует h, такое что a = Subtype.mk b h, если и только если b = a.

LaTeX

$$$@[simp]\ntheorem _root_.exists_subtype_mk_eq_iff {a : Subtype p} {b : \alpha} : (\exists h : p b, Subtype.mk b h = a) \leftrightarrow b = a$$$

Lean4

@[simp]
theorem _root_.exists_subtype_mk_eq_iff {a : Subtype p} {b : α} : (∃ h : p b, Subtype.mk b h = a) ↔ b = a := by grind

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