inter — Mathlib

English

Diophantine sets are closed under intersection: 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 \\cap S') $$$$

Lean4

/-- Diophantine sets are closed under intersection. -/
theorem inter (d : Dioph S) (d' : Dioph S') : Dioph (S ∩ S') :=
  DiophList.forall [S, S'] ⟨d, d'⟩

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