isAtomic_graph — Mathlib

English

Let L be a language and f be an n-ary function symbol in L. The graph of f is an atomic formula in the language L.

Русский

Пусть L — язык, и f — n-арный символь функции в L. Граф функции f является атомарной формулой языка L.

LaTeX

$$$\\operatorname{IsAtomic}(\\mathrm{Graph}(f))$$$

Lean4

theorem isAtomic_graph (f : L.Functions n) : (Formula.graph f).IsAtomic :=
  BoundedFormula.IsAtomic.equal _ _

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