Commit 2022-03-18 16:51 80b8d191

View on Github →

feat(model_theory/terms_and_formulas): Language maps act on terms, formulas, sentences, and theories (#12609) Defines the action of language maps on terms, formulas, sentences, and theories Shows that said action commutes with realization

Estimated changes

Modified src/model_theory/terms_and_formulas.lean

added theorem first_order.language.Lhom.mem_on_Theory

added def first_order.language.Lhom.on_Theory

added theorem first_order.language.Lhom.on_Theory_model

added def first_order.language.Lhom.on_bounded_formula

added def first_order.language.Lhom.on_formula

added def first_order.language.Lhom.on_sentence

added def first_order.language.Lhom.on_term

added theorem first_order.language.Lhom.realize_on_bounded_formula

added theorem first_order.language.Lhom.realize_on_formula

added theorem first_order.language.Lhom.realize_on_sentence

added theorem first_order.language.Lhom.realize_on_term