union — Mathlib

English

Diophantine sets are closed under union: if S and S' are Dioph, then S ∪ S' is Dioph.

Русский

Диофовы множества замкнуты по объединению: если S и S' диофовы, то S ∪ S' диофово.

LaTeX

$$$$ \\text{Dioph}(S) \\to \\text{Dioph}(S') \\to \\text{Dioph}(S \\cup S') $$$$

Lean4

/-- Diophantine sets are closed under union. -/
theorem union : ∀ (_ : Dioph S) (_ : Dioph S'), Dioph (S ∪ S')
  | ⟨β, p, pe⟩, ⟨γ, q, qe⟩ =>
    ⟨β ⊕ γ, p.map (inl ⊗ inr ∘ inl) * q.map (inl ⊗ inr ∘ inr), fun v =>
      by
      refine
        Iff.trans (or_congr ((pe v).trans ?_) ((qe v).trans ?_))
          (exists_or.symm.trans
            (exists_congr fun t =>
              (@mul_eq_zero _ _ _ (p ((v ⊗ t) ∘ (inl ⊗ inr ∘ inl))) (q ((v ⊗ t) ∘ (inl ⊗ inr ∘ inr)))).symm))
      · -- Porting note: putting everything on the same line fails

        refine inject_dummies_lem _ (some ⊗ fun _ => none) ?_ _ _
        exact fun _ => by simp only [elim_inl]
      · -- Porting note: putting everything on the same line fails

        refine inject_dummies_lem _ ((fun _ => none) ⊗ some) ?_ _ _
        exact fun _ => by simp only [elim_inr]⟩

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