term_D∧_ — Mathlib

English

Composition on Diophantine functions preserves Diophantine status when combining with a vector of Diophantine functions.

Русский

Композиция диагофантовых функций сохраняет диагофантовость при объединении с вектором диагофантных функций.

LaTeX

$$$$\mathrm{DiophFn}(f) \Rightarrow \mathrm{Dioph}\left(\{v \mid f(v) \in S\}\right)$$$$

Lean4

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

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