English
Non-dependent recursion principle: liftOn x f H computes the value by recursing on representatives.
Русский
Неподчинённый принцип рекурсии: liftOn x f H вычисляет значение по представителям.
LaTeX
$$$ liftOn\ x\ f\ H \in\, p $$$
Lean4
/-- Non-dependent recursion principle for localizations: given elements `f a b : p`
for all `a b`, such that `r S (a, b) (c, d)` implies `f a b = f c d`,
then `f` is defined on the whole `Localization S`. -/
@[to_additive /-- Non-dependent recursion principle for `AddLocalization`s: given elements `f a b : p`
for all `a b`, such that `r S (a, b) (c, d)` implies `f a b = f c d`,
then `f` is defined on the whole `Localization S`. -/
]
def liftOn {p : Sort u} (x : Localization S) (f : M → S → p)
(H : ∀ {a c : M} {b d : S}, r S (a, b) (c, d) → f a b = f c d) : p :=
rec f (fun h ↦ (by simpa only [eq_rec_constant] using H h)) x
