le_dioph — Mathlib

English

The set {v | f v ≤ g v} is Diophantine when f and g are Diophantine.

Русский

Множество ≤ диагофантово при f,g диагофантовых.

LaTeX

$$$$\mathrm{Dioph}(f) \Rightarrow \mathrm{Dioph}(g) \Rightarrow \mathrm{Dioph}\{v \mid f(v) \le g(v)\}$$$$

Lean4

/-- The set of places where one Diophantine function is at most another is Diophantine. -/
theorem le_dioph : Dioph {v | f v ≤ g v} :=
  dioph_comp2 df dg <| ext ((D∃) 2 <| D&1 D+ D&0 D= D&2) fun _ => ⟨fun ⟨_, hx⟩ => le.intro hx, le.dest⟩

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