liftOn₂ — Mathlib

English

Lift on a two-argument function descends through the localization to a function on LocalizedModule S M.

Русский

Подъем по двум аргументам спускается через локализацию на LocalizedModule S M.

LaTeX

$$$\\text{liftOn}_2 : (M \\times S) \\to (LocalizedModule S M) \\to (LocalizedModule S M) \\to α$$$

Lean4

/-- If `f : M × S → M × S → α` respects the equivalence relation `LocalizedModule.r`, then
`f` descents to a map `LocalizedModule M S → LocalizedModule M S → α`.
-/
def liftOn₂ {α : Type*} (x y : LocalizedModule S M) (f : M × S → M × S → α)
    (wd : ∀ (p q p' q' : M × S), p ≈ p' → q ≈ q' → f p q = f p' q') : α :=
  Quotient.liftOn₂ x y f wd

Похожие утверждения