English
Non-dependent recursion principle for two-variable localization: liftOn₂ x y f H computes on mk representations consistently.
Русский
Неподчинённый принцип рекурсии по двум переменным локализации: liftOn₂ x y f H согласованно вычисляет на представлениях mk.
LaTeX
$$$ liftOn₂\ x\ y\ f\ H = f a b c d $$$
Lean4
/-- Non-dependent recursion principle for localizations: given elements `f x y : p`
for all `x` and `y`, such that `r S x x'` and `r S y y'` implies `f x y = f x' y'`,
then `f` is defined on the whole `Localization S`. -/
@[to_additive /-- Non-dependent recursion principle for localizations: given elements `f x y : p`
for all `x` and `y`, such that `r S x x'` and `r S y y'` implies `f x y = f x' y'`,
then `f` is defined on the whole `Localization S`. -/
]
def liftOn₂ {p : Sort u} (x y : Localization S) (f : M → S → M → S → p)
(H : ∀ {a a' b b' c c' d d'}, r S (a, b) (a', b') → r S (c, d) (c', d') → f a b c d = f a' b' c' d') : p :=
liftOn x (fun a b ↦ liftOn y (f a b) fun hy ↦ H ((r S).refl _) hy) fun hx ↦
induction_on y fun ⟨_, _⟩ ↦ H hx ((r S).refl _)
