Theorems · Theorem · order theory

ArchimedeanClass.ind

∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M]
  {motive : ArchimedeanClass M → Prop},
  (∀ (a : M), motive (ArchimedeanClass.mk a)) → ∀ (x : ArchimedeanClass M), motive x

An induction principle for ArchimedeanClass

Defined in

Mathlib.Algebra.Order.Archimedean.Class

Cited by

3 results in Mathlib

Foundations

Depth 23 from the axioms · uses propext, Quot.sound

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoid