Commit 2023-05-13 14:21 21ac3b50

View on Github →

feat: port ModelTheory.Skolem (#3951)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/Skolem.lean

added theorem FirstOrder.Language.Substructure.coeSort_elementarySkolem₁Reduct

added theorem FirstOrder.Language.Substructure.skolem₁_reduct_isElementary

added theorem FirstOrder.Language.card_functions_sum_skolem₁

added theorem FirstOrder.Language.card_functions_sum_skolem₁_le

added theorem FirstOrder.Language.exists_elementarySubstructure_card_eq

added theorem FirstOrder.Language.exists_small_elementarySubstructure

added def FirstOrder.Language.skolem₁