ex_dioph — Mathlib

English

If S is a Diophantine set of functions from α ⊕ β to ℕ, then the set of v : β ⊕ γ → ℕ for which there exists x with v ⊗ x ∈ S is Diophantine.

Русский

Если S есть Диофантово множество функций из α ⊕ β в ℕ, то множество v : β ⊕ γ → ℕ such that существует x с v ⊗ x ∈ S является диагофантовым.

LaTeX

$$$$\mathrm{Dioph}(S) \Rightarrow \mathrm{Dioph}\left(\{v: \beta \oplus \gamma \to \mathbb{N} \mid \exists x: \alpha \to \mathbb{N},\ v \otimes x \in S\}\right)$$$$

Lean4

theorem ex_dioph {S : Set (α ⊕ β → ℕ)} : Dioph S → Dioph {v | ∃ x, v ⊗ x ∈ S}
  | ⟨γ, p, pe⟩ =>
    ⟨β ⊕ γ, p.map ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr), fun v =>
      ⟨fun ⟨x, hx⟩ =>
        let ⟨t, ht⟩ := (pe _).1 hx
        ⟨x ⊗ t, by
          simp only [Poly.map_apply]
          rw [show (v ⊗ x ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) = (v ⊗ x) ⊗ t from
              funext fun s => by
                rcases s with a | b <;>
                  try { cases a <;> rfl
                  };
                rfl]
          exact ht⟩,
        fun ⟨t, ht⟩ =>
        ⟨t ∘ inl,
          (pe _).2
            ⟨t ∘ inr, by
              simp only [Poly.map_apply] at ht
              rwa [show (v ⊗ t) ∘ ((inl ⊗ inr ∘ inl) ⊗ inr ∘ inr) = (v ⊗ t ∘ inl) ⊗ t ∘ inr from
                  funext fun s => by
                    rcases s with a | b <;>
                      try { cases a <;> rfl
                      };
                    rfl] at ht⟩⟩⟩⟩

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