equivSentence — Mathlib

English

A bijection sending formulas to sentences with constants is established by composing the constants-variables equivalence with a relabeling to constants.

Русский

Существует биекция между формулах и предложениями с константами, образованная композицией эквивалентности констант и переименованием в константы.

LaTeX

$$$\\text{equivSentence} : L.Formula \\alpha \\simeq L[[\\alpha]].Sentence$$$

Lean4

/-- A bijection sending formulas to sentences with constants. -/
def equivSentence : L.Formula α ≃ L[[α]].Sentence :=
  (BoundedFormula.constantsVarsEquiv.trans (BoundedFormula.relabelEquiv (Equiv.sumEmpty _ _))).symm

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