Commit 2022-03-12 18:01 707df2cd

View on Github →

feat(model_theory/definability): Definability with parameters (#12611) Extends the definition of definable sets to include a parameter set. Defines shorthands is_definable₁ and is_definable₂ for 1- and 2-dimensional definable sets.

Estimated changes

Modified src/model_theory/definability.lean

added theorem first_order.language.definable.compl

added theorem first_order.language.definable.image_comp_equiv

added theorem first_order.language.definable.inter

added theorem first_order.language.definable.preimage_comp

added theorem first_order.language.definable.sdiff

added theorem first_order.language.definable.union

added structure first_order.language.definable

added theorem first_order.language.definable_empty

added theorem first_order.language.definable_finset_bInter

added theorem first_order.language.definable_finset_bUnion

added theorem first_order.language.definable_finset_inf

added theorem first_order.language.definable_finset_sup

modified theorem first_order.language.definable_set.coe_bot

modified theorem first_order.language.definable_set.coe_compl

modified theorem first_order.language.definable_set.coe_inf

modified theorem first_order.language.definable_set.coe_sup

modified theorem first_order.language.definable_set.coe_top

modified theorem first_order.language.definable_set.le_iff

modified theorem first_order.language.definable_set.mem_compl

modified theorem first_order.language.definable_set.mem_inf

modified theorem first_order.language.definable_set.mem_sup

modified theorem first_order.language.definable_set.mem_top

modified theorem first_order.language.definable_set.not_mem_bot

modified def first_order.language.definable_set

added theorem first_order.language.definable_univ

added def first_order.language.definable₁

added def first_order.language.definable₂

deleted theorem first_order.language.is_definable.compl

deleted theorem first_order.language.is_definable.inter

deleted theorem first_order.language.is_definable.sdiff

deleted theorem first_order.language.is_definable.union

deleted structure first_order.language.is_definable

deleted theorem first_order.language.is_definable_empty

deleted theorem first_order.language.is_definable_univ