repr_inj — Mathlib

English

The representation map repr is injective on NF elements: if repr a = repr b for NF a and NF b, then a = b (and conversely).

Русский

Образующая отображение repr инъективно на элементах NF: если repr a = repr b для NF a и NF b, то a = b (и наоборот).

LaTeX

$$$\forall a,b : ONote\,[a.NF][b.NF],\; (repr\; a = repr\; b) \iff a = b$$$

Lean4

theorem repr_inj {a b} [NF a] [NF b] : repr a = repr b ↔ a = b :=
  ⟨fun e =>
    match cmp a b, cmp_compares a b with
    | Ordering.lt, (h : repr a < repr b) => (ne_of_lt h e).elim
    | Ordering.gt, (h : repr a > repr b) => (ne_of_gt h e).elim
    | Ordering.eq, h => h,
    congr_arg _⟩

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