Commit 2023-04-18 11:12 a372cbf8

View on Github →

feat: port ModelTheory.Encoding (#3494)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/Encoding.lean

added theorem FirstOrder.Language.BoundedFormula.card_le

added def FirstOrder.Language.BoundedFormula.listDecode

added theorem FirstOrder.Language.BoundedFormula.listDecode_encode_list

added def FirstOrder.Language.BoundedFormula.listEncode

added theorem FirstOrder.Language.BoundedFormula.listEncode_sigma_injective

added def FirstOrder.Language.BoundedFormula.sigmaAll

added def FirstOrder.Language.BoundedFormula.sigmaImp

added theorem FirstOrder.Language.Term.card_le

added theorem FirstOrder.Language.Term.card_sigma

added def FirstOrder.Language.Term.listDecode

added theorem FirstOrder.Language.Term.listDecode_encode_list

added def FirstOrder.Language.Term.listEncode

added theorem FirstOrder.Language.Term.listEncode_injective