term_D=_ — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[inherit_doc Dioph.eq_dioph, scoped term_parser 1000]
public meta def «term_D=_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `Dioph.«term_D=_» 50 50
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " D= ") (ParserDescr.cat✝ `term 51))

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