ne_dioph — Mathlib

English

The set {v | f v ≠ g v} is Diophantine if f and g are Diophantine.

Русский

Множество {v | f(v) ≠ g(v)} диагофантово при диагофантовых f,g.

LaTeX

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

Lean4

/-- The set of places where two Diophantine functions are unequal is Diophantine. -/
theorem ne_dioph : Dioph {v | f v ≠ g v} :=
  ext (df D< dg D∨ dg D< df) fun v => by dsimp; exact lt_or_lt_iff_ne (α := ℕ)

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