Commit 2023-04-17 11:39 ed47d42a

View on Github →

feat: port ModelTheory.Syntax (#3195)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/Syntax.lean

added theorem FirstOrder.Language.BoundedFormula.IsAtomic.castLE

added theorem FirstOrder.Language.BoundedFormula.IsAtomic.isPrenex

added theorem FirstOrder.Language.BoundedFormula.IsAtomic.isQF

added theorem FirstOrder.Language.BoundedFormula.IsAtomic.liftAt

added theorem FirstOrder.Language.BoundedFormula.IsAtomic.relabel

added inductive FirstOrder.Language.BoundedFormula.IsAtomic

added theorem FirstOrder.Language.BoundedFormula.IsPrenex.castLE

added theorem FirstOrder.Language.BoundedFormula.IsPrenex.induction_on_all_not

added theorem FirstOrder.Language.BoundedFormula.IsPrenex.liftAt

added theorem FirstOrder.Language.BoundedFormula.IsPrenex.relabel

added inductive FirstOrder.Language.BoundedFormula.IsPrenex

added theorem FirstOrder.Language.BoundedFormula.IsQF.castLE

added theorem FirstOrder.Language.BoundedFormula.IsQF.isPrenex

added theorem FirstOrder.Language.BoundedFormula.IsQF.liftAt

added theorem FirstOrder.Language.BoundedFormula.IsQF.not

added theorem FirstOrder.Language.BoundedFormula.IsQF.relabel

added theorem FirstOrder.Language.BoundedFormula.IsQF.toPrenexImp

added theorem FirstOrder.Language.BoundedFormula.IsQF.toPrenexImpRight

added inductive FirstOrder.Language.BoundedFormula.IsQF

added def FirstOrder.Language.BoundedFormula.alls

added def FirstOrder.Language.BoundedFormula.castLE

added theorem FirstOrder.Language.BoundedFormula.castLE_castLE

added theorem FirstOrder.Language.BoundedFormula.castLE_comp_castLE

added theorem FirstOrder.Language.BoundedFormula.castLE_rfl

added def FirstOrder.Language.BoundedFormula.constantsVarsEquiv

added def FirstOrder.Language.BoundedFormula.exs

added def FirstOrder.Language.BoundedFormula.freeVarFinset

added theorem FirstOrder.Language.BoundedFormula.isPrenex_toPrenexImp

added theorem FirstOrder.Language.BoundedFormula.isPrenex_toPrenexImpRight

added theorem FirstOrder.Language.BoundedFormula.isQF_bot

added def FirstOrder.Language.BoundedFormula.liftAt

added def FirstOrder.Language.BoundedFormula.mapTermRel

added def FirstOrder.Language.BoundedFormula.mapTermRelEquiv

added theorem FirstOrder.Language.BoundedFormula.mapTermRel_id_id_id

added theorem FirstOrder.Language.BoundedFormula.mapTermRel_mapTermRel

added theorem FirstOrder.Language.BoundedFormula.not_all_isAtomic

added theorem FirstOrder.Language.BoundedFormula.not_all_isQF

added theorem FirstOrder.Language.BoundedFormula.not_ex_isAtomic

added theorem FirstOrder.Language.BoundedFormula.not_ex_isQF

added def FirstOrder.Language.BoundedFormula.relabel

added def FirstOrder.Language.BoundedFormula.relabelAux

added theorem FirstOrder.Language.BoundedFormula.relabelAux_sum_inl

added def FirstOrder.Language.BoundedFormula.relabelEquiv

added theorem FirstOrder.Language.BoundedFormula.relabel_all

added theorem FirstOrder.Language.BoundedFormula.relabel_bot

added theorem FirstOrder.Language.BoundedFormula.relabel_ex

added theorem FirstOrder.Language.BoundedFormula.relabel_falsum

added theorem FirstOrder.Language.BoundedFormula.relabel_imp

added theorem FirstOrder.Language.BoundedFormula.relabel_not

added theorem FirstOrder.Language.BoundedFormula.relabel_sum_inl

added def FirstOrder.Language.BoundedFormula.restrictFreeVar

added def FirstOrder.Language.BoundedFormula.subst

added theorem FirstOrder.Language.BoundedFormula.sum_elim_comp_relabelAux

added def FirstOrder.Language.BoundedFormula.toFormula

added def FirstOrder.Language.BoundedFormula.toPrenex

added def FirstOrder.Language.BoundedFormula.toPrenexImp

added def FirstOrder.Language.BoundedFormula.toPrenexImpRight

added theorem FirstOrder.Language.BoundedFormula.toPrenex_isPrenex

added inductive FirstOrder.Language.BoundedFormula

added def FirstOrder.Language.Constants.term

added def FirstOrder.Language.Formula.equivSentence

added theorem FirstOrder.Language.Formula.equivSentence_inf

added theorem FirstOrder.Language.Formula.equivSentence_not

added def FirstOrder.Language.Formula.graph

added theorem FirstOrder.Language.Formula.isAtomic_graph

added def FirstOrder.Language.Formula.relabel

added def FirstOrder.Language.Formula

added def FirstOrder.Language.Functions.apply₁

added def FirstOrder.Language.Functions.apply₂

added def FirstOrder.Language.LEquiv.onBoundedFormula

added theorem FirstOrder.Language.LEquiv.onBoundedFormula_symm

added def FirstOrder.Language.LEquiv.onFormula

added theorem FirstOrder.Language.LEquiv.onFormula_apply

added theorem FirstOrder.Language.LEquiv.onFormula_symm

added def FirstOrder.Language.LEquiv.onSentence

added theorem FirstOrder.Language.LHom.comp_onBoundedFormula

added theorem FirstOrder.Language.LHom.comp_onTerm

added theorem FirstOrder.Language.LHom.id_onBoundedFormula

added theorem FirstOrder.Language.LHom.id_onTerm

added theorem FirstOrder.Language.LHom.mem_onTheory

added def FirstOrder.Language.LHom.onBoundedFormula

added def FirstOrder.Language.LHom.onFormula

added def FirstOrder.Language.LHom.onSentence

added def FirstOrder.Language.LHom.onTerm

added def FirstOrder.Language.LHom.onTheory

added def FirstOrder.Language.Lequiv.onTerm

added def FirstOrder.Language.Relations.boundedFormula

added def FirstOrder.Language.Relations.boundedFormula₁

added def FirstOrder.Language.Relations.boundedFormula₂

added def FirstOrder.Language.Relations.formula

added def FirstOrder.Language.Relations.formula₁

added def FirstOrder.Language.Relations.formula₂

added def FirstOrder.Language.Sentence

added def FirstOrder.Language.Term.bdEqual

added def FirstOrder.Language.Term.constantsToVars

added def FirstOrder.Language.Term.constantsVarsEquiv

added def FirstOrder.Language.Term.constantsVarsEquivLeft

added theorem FirstOrder.Language.Term.constantsVarsEquivLeft_apply

added theorem FirstOrder.Language.Term.constantsVarsEquivLeft_symm_apply

added def FirstOrder.Language.Term.equal

added def FirstOrder.Language.Term.liftAt

added def FirstOrder.Language.Term.relabel

added def FirstOrder.Language.Term.relabelEquiv

added theorem FirstOrder.Language.Term.relabel_comp_relabel

added theorem FirstOrder.Language.Term.relabel_id

added theorem FirstOrder.Language.Term.relabel_id_eq_id

added theorem FirstOrder.Language.Term.relabel_relabel

added def FirstOrder.Language.Term.restrictVar

added def FirstOrder.Language.Term.restrictVarLeft

added def FirstOrder.Language.Term.subst

added def FirstOrder.Language.Term.varFinset

added def FirstOrder.Language.Term.varFinsetLeft

added def FirstOrder.Language.Term.varsToConstants

added inductive FirstOrder.Language.Term

added def FirstOrder.Language.Theory

added theorem FirstOrder.Language.directed_distinctConstantsTheory

added def FirstOrder.Language.distinctConstantsTheory

added theorem FirstOrder.Language.distinctConstantsTheory_eq_unionᵢ

added def FirstOrder.Language.infiniteTheory

added theorem FirstOrder.Language.monotone_distinctConstantsTheory

added def FirstOrder.Language.nonemptyTheory