liftOn — Mathlib

English

If two representatives are equivalent, lifting preserves equality of the function values.

Русский

Если две представительские пары эквивалентны, поднятие сохраняет равенство значений функции.

LaTeX

$$$x = y \\Rightarrow \\text{liftOn}\\,f\\,wd\\; x = \\text{liftOn}\\,f\\,wd\\; y$$$

Lean4

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

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