liftOn — Mathlib

English

Lifts a function on sets of natural numbers to an element of φ on ManyOneDegree, respecting equivalence classes.

Русский

Переносит функцию на множества натуральных чисел в элемент φ над ManyOneDegree, сохраняет эквивалентности.

LaTeX

$$$ \\mathrm{liftOn} : \\{d : ManyOneDegree\\} \\to (\\{f : Set\\\\ Nat \\to \\phi\\}) \\to (\\\\forall p q, ManyOneEquiv p q \\\\to f p = f q) \\\\to \\phi $$$

Lean4

/-- Lifts a function on sets of natural numbers to many-one degrees. -/
protected abbrev liftOn {φ} (d : ManyOneDegree) (f : Set ℕ → φ) (h : ∀ p q, ManyOneEquiv p q → f p = f q) : φ :=
  Quotient.liftOn' d f h

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