ex — Mathlib · SciLib

English

The bounded formulas admit a top element which can be defined via negation of a bottom, generating a maximal element in the poset of bounded formulas.

Русский

Ограниченные формулы образуют верхний элемент, который можно определить через отрицание нуля, образуя максимальный элемент частично упорядоченного множества.

LaTeX

$$$\\text{Top}(L.BoundedFormula\\;\\alpha\\; n) = \\langle \\mathrm{BoundedFormula.not} \\; \\bot\\rangle$$$

Lean4

/-- Puts an `∃` quantifier on a bounded formula. -/
@[match_pattern]
protected def ex (φ : L.BoundedFormula α (n + 1)) : L.BoundedFormula α n :=
  φ.not.all.not

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