instIsTotalLe — Mathlib

English

There is an induction principle for MulArchimedeanClass: to prove a property for all classes, it suffices to prove it for every mk a with a ∈ M.

Русский

Существует принцип индукции по ArchimedeanClass: чтобы доказать свойство для всех классов, достаточно доказать его для каждого mk a.

LaTeX

$$$\forall x\in MulArchimedeanClass M, \; P(x)$ follows from $\forall a\in M,\; P(mk(a))$.$$

Lean4

@[to_additive]
instance : IsTotal (MulArchimedeanOrder M) (· ≤ ·) where
  total a
    b := by
    obtain hab | hab := le_total |a.val|ₘ |b.val|ₘ
    · exact .inr ⟨1, by simpa using hab⟩
    · exact .inl ⟨1, by simpa using hab⟩

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