English
Lifts a binary function on sets to ManyOneDegree, compatible with equivalence relations.
Русский
Переносит двичную функцию на множества в ManyOneDegree, совместим с эквивалентностями.
LaTeX
$$$ \\mathrm{liftOn}_2 : \\{f : Set\\\\ Nat \\to Set\\\\ Nat \\to \\phi\\} \\to \\text{(compatibility condition)} \\to \\phi $$$
Lean4
/-- Lifts a binary function on sets of natural numbers to many-one degrees. -/
@[reducible, simp]
protected def liftOn₂ {φ} (d₁ d₂ : ManyOneDegree) (f : Set ℕ → Set ℕ → φ)
(h : ∀ p₁ p₂ q₁ q₂, ManyOneEquiv p₁ p₂ → ManyOneEquiv q₁ q₂ → f p₁ q₁ = f p₂ q₂) : φ :=
d₁.liftOn (fun p => d₂.liftOn (f p) fun _ _ hq => h _ _ _ _ (by rfl) hq)
(by
intro p₁ p₂ hp
induction d₂ using ManyOneDegree.ind_on
apply h
· assumption
· rfl)
