coe_eq_coe — Mathlib

English

The natural embedding of α into WithTop(α) is injective: a maps to the same element in WithTop(α) only if a=b.

Русский

Естественное вложение α в WithTop(α) инъективно: отображение удовлетворяет: a=b, если a и b соответствуют одному элементу внутри WithTop(α).

LaTeX

$$$\\forall a,b:\\; (a:\\mathrm{WithTop}(\\alpha)) = (b) \\iff a=b$$$

Lean4

@[simp, norm_cast]
theorem coe_eq_coe : (a : WithTop α) = b ↔ a = b :=
  Option.some_inj

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