instTop

Mathlib.ModelTheory.Syntax

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.BoundedFormula.instTop

English

Negation of a bounded formula is again a bounded formula, formed by taking the implication to falsum.

Русский

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

LaTeX

$$$$\\text{Not}(\\varphi) := \\varphi\\.imp(\\bot)$$$$

Lean4

instance : Top (L.BoundedFormula α n) :=
  ⟨BoundedFormula.not ⊥⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru