Commit 2023-05-25 11:24 e67b5cfb

View on Github →

feat: port ModelTheory.Types (#3991)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/Types.lean

added theorem FirstOrder.Language.Theory.CompleteType.compl_setOf_mem

added theorem FirstOrder.Language.Theory.CompleteType.formula_mem_typeOf

added theorem FirstOrder.Language.Theory.CompleteType.iInter_setOf_subset

added theorem FirstOrder.Language.Theory.CompleteType.isMaximal

added theorem FirstOrder.Language.Theory.CompleteType.mem_of_models

added theorem FirstOrder.Language.Theory.CompleteType.mem_or_not_mem

added theorem FirstOrder.Language.Theory.CompleteType.mem_typeOf

added theorem FirstOrder.Language.Theory.CompleteType.nonempty_iff

added theorem FirstOrder.Language.Theory.CompleteType.not_mem_iff

added theorem FirstOrder.Language.Theory.CompleteType.setOf_mem_eq_univ_iff

added theorem FirstOrder.Language.Theory.CompleteType.setOf_subset_eq_empty_iff

added theorem FirstOrder.Language.Theory.CompleteType.setOf_subset_eq_univ_iff

added theorem FirstOrder.Language.Theory.CompleteType.subset

added theorem FirstOrder.Language.Theory.CompleteType.toList_foldr_inf_mem

added structure FirstOrder.Language.Theory.CompleteType

added theorem FirstOrder.Language.Theory.exists_modelType_is_realized_in

added def FirstOrder.Language.Theory.realizedTypes

added def FirstOrder.Language.Theory.typeOf