English
Lift lifts a function f: M → α to MulArchimedeanClass M → α, provided it respects mk-equivalence: f a = f b whenever mk a = mk b.
Русский
Lift поднимает функцию f: M → α до MulArchimedeanClass M → α, если она сохраняет эквиваленцию mk: f a = f b, когда mk a = mk b.
LaTeX
$$$lift:f: M \to \alpha,\ h: \forall a,b, mk a = mk b \Rightarrow f a = f b \quad\Rightarrow\quad MulArchimedeanClass M \to \alpha$$$
Lean4
/-- Lift a `M → α` function to `MulArchimedeanClass M → α`. -/
@[to_additive /-- Lift a `M → α` function to `ArchimedeanClass M → α`. -/
]
def lift {α : Type*} (f : M → α) (h : ∀ a b, mk a = mk b → f a = f b) : MulArchimedeanClass M → α :=
Quotient.lift f fun _ _ h' ↦ h _ _ <| mk_eq_mk.mpr h'
