reindex_dioph — Mathlib

English

If f : (α → ℕ) → ℕ is Diophantine, then f ∘ g is Diophantine for any g : α → β.

Русский

Если f : (α → ℕ) → ℕ диофантен, то f ∘ g диофантна для любого g : α → β.

LaTeX

$$$$ \\forall f:\\, (α \\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_dioph (f : α → β) : Dioph S → Dioph {v | v ∘ f ∈ S}
  | ⟨γ, p, pe⟩ =>
    ⟨γ, p.map (inl ∘ f ⊗ inr), fun v =>
      (pe _).trans <|
        exists_congr fun t =>
          suffices v ∘ f ⊗ t = (v ⊗ t) ∘ (inl ∘ f ⊗ inr) by simp [this]
          funext fun s => by rcases s with a | b <;> rfl⟩

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