cmp_compares — Mathlib

English

For all a,b in NONote, (cmp a b).Compares a b.

Русский

Для любых a,b ∈ NONote выполняется (cmp a b).Compares a b.

LaTeX

$$$$ \forall a,b \in \text{NONote},\ (cmp(a,b)).\text{Compares } a \ b. $$$$

Lean4

theorem cmp_compares : ∀ a b : NONote, (cmp a b).Compares a b
  | ⟨a, ha⟩, ⟨b, hb⟩ => by
    dsimp [cmp]
    have := ONote.cmp_compares a b
    cases h : ONote.cmp a b <;> simp only [h] at this <;> try exact this
    exact Subtype.mk_eq_mk.2 this

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