Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-23 04:01 264dd7ff

View on Github →

feat(model_theory/basic): Language operations (#12129) Defines language homomorphisms with first_order.language.Lhom Defines the sum of two languages with first_order.language.sum Defines first_order.language.with_constants, a language with added constants, abbreviated L[[A]]. Defines a L[[A]].Structure on M when A : set M. (Some of this code comes from the Flypitch project)

Estimated changes

Modified src/model_theory/basic.lean

added def first_order.language.Lhom.add_constants

added def first_order.language.Lhom.comp

added theorem first_order.language.Lhom.comp_id

added def first_order.language.Lhom.constants_on_map

added theorem first_order.language.Lhom.id_comp

added theorem first_order.language.Lhom.map_constants_comp_with_constants

added def first_order.language.Lhom.sum_elim

added def first_order.language.Lhom.sum_map

added structure first_order.language.Lhom

added def first_order.language.Lhom_trim_empty_constants

added def first_order.language.Lhom_with_constants

added def first_order.language.Lhom_with_constants_map

deleted def first_order.language.const

added def first_order.language.constants_on.Structure

added def first_order.language.constants_on

added theorem first_order.language.constants_on_constants

added def first_order.language.constants_on_functions

added theorem first_order.language.constants_on_map_is_expansion_on

deleted theorem first_order.language.embedding.map_const

added theorem first_order.language.embedding.map_constants

deleted theorem first_order.language.equiv.map_const

added theorem first_order.language.equiv.map_constants

deleted theorem first_order.language.fun_map_eq_coe_const

added theorem first_order.language.fun_map_eq_coe_constants

added theorem first_order.language.fun_map_sum_inl

added theorem first_order.language.fun_map_sum_inr

deleted theorem first_order.language.hom.map_const

added theorem first_order.language.hom.map_constants

modified theorem first_order.language.nonempty_of_nonempty_constants

added theorem first_order.language.rel_map_sum_inl

added theorem first_order.language.rel_map_sum_inr

added def first_order.language.symbols

added def first_order.language.with_constants

Modified src/model_theory/elementary_maps.lean

deleted theorem first_order.language.elementary_embedding.map_const

added theorem first_order.language.elementary_embedding.map_constants

Modified src/model_theory/substructures.lean

deleted theorem first_order.language.substructure.const_mem

added theorem first_order.language.substructure.constants_mem

Modified src/model_theory/terms_and_formulas.lean