reindex_diophFn — Mathlib

English

If f is Diophantine as a function, then f after precomposition with g is also Diophantine.

Русский

Если f диофантна как функция, то f после предобразования через g также диофантна.

LaTeX

$$$$ \\forall f:\\, (\\alpha \\to \\mathbb{N}) \\to \\mathbb{N}, \\forall g:\\, \\alpha \\to \\beta, \\text{DiophFn}(f) \\to \\text{DiophFn}(\\lambda v. f(v \\circ g)) $$$$

Lean4

theorem reindex_diophFn {f : (α → ℕ) → ℕ} (g : α → β) (d : DiophFn f) : DiophFn fun v => f (v ∘ g) := by
  convert reindex_dioph (Option β) (Option.map g) d

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