Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-21 12:46 135c5742

View on Github →

feat(model_theory/definability): Definability lemmas (#12262) Proves several lemmas to work with definability over different parameter sets. Shows that definability is closed under projection.

Estimated changes

Modified src/model_theory/definability.lean

added theorem set.definable.image_comp

added theorem set.definable.image_comp_embedding

added theorem set.definable.image_comp_sum_inl_fin

added theorem set.definable.map_expansion

added theorem set.definable.mono

added theorem set.definable_iff_empty_definable_with_params

added theorem set.empty_definable_iff

added theorem set.fin.coe_cast_add_zero

Modified src/model_theory/terms_and_formulas.lean

modified def first_order.language.Lhom.on_bounded_formula

modified def first_order.language.Lhom.on_formula

modified def first_order.language.Lhom.on_term