Commit 2023-05-12 16:00 6887ea28

View on Github →

feat: port ModelTheory.Definability (#3909)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/Definability.lean

added theorem FirstOrder.Language.DefinableSet.coe_bot

added theorem FirstOrder.Language.DefinableSet.coe_compl

added theorem FirstOrder.Language.DefinableSet.coe_inf

added theorem FirstOrder.Language.DefinableSet.coe_sdiff

added theorem FirstOrder.Language.DefinableSet.coe_sup

added theorem FirstOrder.Language.DefinableSet.coe_top

added theorem FirstOrder.Language.DefinableSet.le_iff

added theorem FirstOrder.Language.DefinableSet.mem_compl

added theorem FirstOrder.Language.DefinableSet.mem_inf

added theorem FirstOrder.Language.DefinableSet.mem_sdiff

added theorem FirstOrder.Language.DefinableSet.mem_sup

added theorem FirstOrder.Language.DefinableSet.mem_top

added theorem FirstOrder.Language.DefinableSet.not_mem_bot

added def FirstOrder.Language.DefinableSet

added theorem Set.Definable.compl

added theorem Set.Definable.image_comp

added theorem Set.Definable.image_comp_embedding

added theorem Set.Definable.image_comp_equiv

added theorem Set.Definable.image_comp_sum_inl_fin

added theorem Set.Definable.inter

added theorem Set.Definable.map_expansion

added theorem Set.Definable.mono

added theorem Set.Definable.preimage_comp

added theorem Set.Definable.sdiff

added theorem Set.Definable.union

added def Set.Definable

added def Set.Definable₁

added def Set.Definable₂

added theorem Set.definable_empty

added theorem Set.definable_finset_binterᵢ

added theorem Set.definable_finset_bunionᵢ

added theorem Set.definable_finset_inf

added theorem Set.definable_finset_sup

added theorem Set.definable_iff_empty_definable_with_params

added theorem Set.definable_univ

added theorem Set.empty_definable_iff