onSentence — Mathlib

English

The onSentence map lifts the onFormula map to sentences along a language equivalence.

Русский

Отображение onSentence поднимает отображение onFormula к предложениям через эквивалентность языка.

LaTeX

$$$\\text{onSentence} : L.Equiv L' \\to (L.Sentence \\to L'.Sentence)$$$

Lean4

/-- Maps a sentence's symbols along a language equivalence. -/
@[simps!]
def onSentence (φ : L ≃ᴸ L') : L.Sentence ≃ L'.Sentence :=
  φ.onFormula

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