Commit 2022-03-11 16:25 003701f0

View on Github →

feat(model_theory/substructures): Facts about substructures (#12258) Shows that closure L s can be viewed as the set of realizations of terms over s. Bounds the cardinality of closure L s by the cardinality of the type of terms. Characterizes closure L[[A]] s.

Estimated changes

Modified src/model_theory/substructures.lean

added theorem first_order.language.Lhom.coe_substructure_reduct

added theorem first_order.language.Lhom.mem_substructure_reduct

added def first_order.language.Lhom.substructure_reduct

added theorem first_order.language.substructure.closure_with_constants_eq

added theorem first_order.language.substructure.coe_closure_eq_range_term_realize

added theorem first_order.language.substructure.coe_with_constants

modified theorem first_order.language.substructure.constants_mem

added theorem first_order.language.substructure.lift_card_closure_le

added theorem first_order.language.substructure.lift_card_closure_le_card_term

added theorem first_order.language.substructure.mem_closure_iff_exists_term

added theorem first_order.language.substructure.mem_with_constants

added theorem first_order.language.substructure.reduct_with_constants

added theorem first_order.language.substructure.subset_closure_with_constants

added def first_order.language.substructure.with_constants

added theorem first_order.language.term.realize_mem