English
There is an order-preserving lift from {a ≠ 1} to FiniteMulArchimedeanClass M to any α, given a monotone base function f on representatives.
Русский
Существует возрастоподдерживающее поднятие из {a ≠ 1} в FiniteMulArchimedeanClass M в любой тип α, заданное монотонной базовой функцией f.
LaTeX
$$$\text{liftOrderHom } f h : FiniteMulArchimedeanClass M \too α$$$
Lean4
/-- Lift a function `{a : M // a ≠ 1} → α` that's monotone along archimedean classes to a
monotone function `FiniteMulArchimedeanClass M →o α`. -/
@[to_additive /-- Lift a function `{a : M // a ≠ 1} → α` that's monotone along archimedean
classes to a monotone function `FiniteArchimedeanClass M₁ →o α`. -/
]
noncomputable def liftOrderHom {α : Type*} [PartialOrder α] (f : { a : M // a ≠ 1 } → α)
(h : ∀ (a b : { a : M // a ≠ 1 }), mk a.val a.prop ≤ mk b.val b.prop → f a ≤ f b) : FiniteMulArchimedeanClass M →o α
where
toFun := lift f fun a b heq ↦ le_antisymm (h a b heq.le) (h b a heq.ge)
monotone' A B
hAB :=
by
induction A using ind with
| mk a ha
induction B using ind with
| mk b hb
simpa using h ⟨a, ha⟩ ⟨b, hb⟩ hAB
