Theorems · Theorem · order theory

FiniteArchimedeanClass.liftOrderHom_mk

∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {α : Type u_2}
  [inst_3 : PartialOrder α] (f : { a // a ≠ 0 } → α)
  (h : ∀ (a b : { a // a ≠ 0 }), FiniteArchimedeanClass.mk ↑a ⋯ ≤ FiniteArchimedeanClass.mk ↑b ⋯ → f a ≤ f b) {a : M}
  (ha : a ≠ 0), (FiniteArchimedeanClass.liftOrderHom f h) (FiniteArchimedeanClass.mk a ha) = f ⟨a, ha⟩

Defined in

Mathlib.Algebra.Order.Archimedean.Class

Cited by

2 results in Mathlib

Foundations

Depth 43 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommGroupLinearOrderIsOrderedAddMonoidPartialOrder