English
Maps a bounded formula along a language map L→ᴸ L′, preserving the structure of falsum, equality, relation, implication, and universal quantification.
Русский
Переводит ограниченную формулу вдоль отображения языка L в язык L′, сохраняя структуру falsum, равенство, отношение, импликацию и всеобщность.
LaTeX
$$$\\text{onBoundedFormula }(g): \\forall k, L.BoundedFormula \\to L'.BoundedFormula$ defined by cases on Falsum, Equal, Rel, Imp, All$$$
Lean4
/-- Maps a bounded formula's symbols along a language map. -/
@[simp]
def onBoundedFormula (g : L →ᴸ L') : ∀ {k : ℕ}, L.BoundedFormula α k → L'.BoundedFormula α k
| _k, falsum => falsum
| _k, equal t₁ t₂ => (g.onTerm t₁).bdEqual (g.onTerm t₂)
| _k, rel R ts => (g.onRelation R).boundedFormula (g.onTerm ∘ ts)
| _k, imp f₁ f₂ => (onBoundedFormula g f₁).imp (onBoundedFormula g f₂)
| _k, all f => (onBoundedFormula g f).all
