term_⇔[_]_ — Mathlib

English

Two bounded formulas are equivalent w.r.t. T if they have identical realizations across all models of T.

Русский

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

LaTeX

$$$T.\\mathrm{Iff}(φ, ψ) \\equiv (T.ModelsBoundedFormula (φ.iff ψ))$$$

Lean4

@[inherit_doc FirstOrder.Language.Theory.Iff, scoped term_parser 1000]
public meta def «term_⇔[_]_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `FirstOrder.«term_⇔[_]_» 51 50
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " ⇔[") (ParserDescr.cat✝ `term 0))
        (ParserDescr.symbol✝ "] "))
      (ParserDescr.cat✝ `term 51))

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