instMax

Mathlib.ModelTheory.Syntax

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

English

The same collection carries a join operation, i.e. φ ∨ ψ := ¬φ → ψ.

Русский

Та же коллекция имеет объединение: φ ∨ ψ = ¬φ → ψ.

LaTeX

$$$\forall \phi, \psi \in L.BoundedFormula\,\alpha\,n,\; \phi \lor \psi = (\neg \phi) \to \psi$$$

Lean4

instance : Max (L.BoundedFormula α n) :=
  ⟨fun f g => f.not.imp g⟩

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

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

Разделы

Аффилиация

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