Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-18 18:32 f4e7f82a

View on Github →

chore(model_theory/definability): Change variable order in definability (#12802) Changes first_order.language.definable and first_order.language.definable_set to set.definable and set.definable_set. Makes set.definable a def rather than a structure.

Estimated changes

Modified docs/overview.yaml

Modified src/model_theory/definability.lean

deleted theorem first_order.language.definable.compl

deleted theorem first_order.language.definable.image_comp_equiv

deleted theorem first_order.language.definable.inter

deleted theorem first_order.language.definable.preimage_comp

deleted theorem first_order.language.definable.sdiff

deleted theorem first_order.language.definable.union

deleted structure first_order.language.definable

deleted theorem first_order.language.definable_empty

deleted theorem first_order.language.definable_finset_bInter

deleted theorem first_order.language.definable_finset_bUnion

deleted theorem first_order.language.definable_finset_inf

deleted theorem first_order.language.definable_finset_sup

modified def first_order.language.definable_set

deleted theorem first_order.language.definable_univ

deleted def first_order.language.definable₁

deleted def first_order.language.definable₂

added theorem set.definable.compl

added theorem set.definable.image_comp_equiv

added theorem set.definable.inter

added theorem set.definable.preimage_comp

added theorem set.definable.sdiff

added theorem set.definable.union

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_univ

added def set.definable₁

added def set.definable₂