instMin — Mathlib

English

The family of bounded formulas L.BoundedFormula α n is a lattice under entailment, and the meet (greatest lower bound) is given by φ ∧ ψ := ¬(φ → ¬ψ).

Русский

Множество ограниченных формул L.BoundedFormula α n образует решётку по выводу, причём встреча двух формул равна ¬(φ → ¬ψ).

LaTeX

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

Lean4

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

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