instBot

Mathlib.ModelTheory.Syntax

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

English

The set of bounded formulas is equipped with a bottom element, given by falsum, forming a bottomed structure.

Русский

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

LaTeX

$$$\\text{Bot} (L.BoundedFormula\\;\\alpha\\; n) = \\langle \\mathrm{falsum} \\rangle$$$

Lean4

instance : Bot (L.BoundedFormula α n) :=
  ⟨falsum⟩

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

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

Разделы

Аффилиация

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