ext

Mathlib.NumberTheory.Dioph

URI: https://scilib.ai/kg/mathlib#Dioph.ext

English

If S is Diophantine, then the set {v | v ∘ f ∈ S} is Diophantine.

Русский

Если S Диофово, то множество {v | v ∘ f ∈ S} также диофово.

LaTeX

$$$$ \\text{Dioph}(S) \\;\\rightarrow\\; \\text{Dioph}\\{v : \\alpha \\to \\mathbb{N} \\mid v \\circ f \\in S\\} $$$$

Lean4

theorem ext (d : Dioph S) (H : ∀ v, v ∈ S ↔ v ∈ S') : Dioph S' := by rwa [← Set.ext H]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru