Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-17 00:23 641a9d30

View on Github →

feat(model_theory/basic): Substructures (#7762) Defines substructures of first-order structures

Estimated changes

Modified src/model_theory/basic.lean

added theorem first_order.language.closed_under.Inf

added theorem first_order.language.closed_under.inf

added theorem first_order.language.closed_under.inter

added def first_order.language.closed_under

added theorem first_order.language.embedding.map_const

added theorem first_order.language.equiv.map_const

added theorem first_order.language.fun_map_eq_coe_const

added def first_order.language.hom.eq_locus

added theorem first_order.language.hom.eq_of_eq_on_dense

added theorem first_order.language.hom.eq_of_eq_on_top

added theorem first_order.language.hom.eq_on_closure

added theorem first_order.language.hom.map_const

added theorem first_order.language.substructure.closed

added def first_order.language.substructure.closure

added theorem first_order.language.substructure.closure_Union

added theorem first_order.language.substructure.closure_empty

added theorem first_order.language.substructure.closure_eq

added theorem first_order.language.substructure.closure_eq_of_le

added theorem first_order.language.substructure.closure_induction

added theorem first_order.language.substructure.closure_le

added theorem first_order.language.substructure.closure_mono

added theorem first_order.language.substructure.closure_union

added theorem first_order.language.substructure.closure_univ

added theorem first_order.language.substructure.coe_Inf

added theorem first_order.language.substructure.coe_copy

added theorem first_order.language.substructure.coe_inf

added theorem first_order.language.substructure.coe_infi

added theorem first_order.language.substructure.coe_top

added theorem first_order.language.substructure.const_mem

added theorem first_order.language.substructure.copy_eq

added theorem first_order.language.substructure.dense_induction

added theorem first_order.language.substructure.ext

added theorem first_order.language.substructure.mem_Inf

added theorem first_order.language.substructure.mem_carrier

added theorem first_order.language.substructure.mem_closure

added theorem first_order.language.substructure.mem_inf

added theorem first_order.language.substructure.mem_infi

added theorem first_order.language.substructure.mem_top

added def first_order.language.substructure.simps.coe

added theorem first_order.language.substructure.subset_closure

added structure first_order.language.substructure