Commit 2023-05-12 16:00 6e1a2ec5

View on Github →

feat: port ModelTheory.Substructures (#3913)

Estimated changes

Modified Mathlib.lean

Created Mathlib/ModelTheory/Substructures.lean

added theorem FirstOrder.Language.ClosedUnder.inf

added theorem FirstOrder.Language.ClosedUnder.infₛ

added theorem FirstOrder.Language.ClosedUnder.inter

added def FirstOrder.Language.ClosedUnder

added def FirstOrder.Language.Embedding.codRestrict

added theorem FirstOrder.Language.Embedding.codRestrict_apply

added theorem FirstOrder.Language.Embedding.comp_codRestrict

added def FirstOrder.Language.Embedding.domRestrict

added theorem FirstOrder.Language.Embedding.domRestrict_apply

added theorem FirstOrder.Language.Embedding.equivRange_apply

added theorem FirstOrder.Language.Embedding.substructureEquivMap_apply

added theorem FirstOrder.Language.Embedding.subtype_comp_codRestrict

added theorem FirstOrder.Language.Equiv.toHom_range

added def FirstOrder.Language.Hom.codRestrict

added theorem FirstOrder.Language.Hom.comp_codRestrict

added def FirstOrder.Language.Hom.domRestrict

added def FirstOrder.Language.Hom.eqLocus

added theorem FirstOrder.Language.Hom.eqOn_closure

added theorem FirstOrder.Language.Hom.eq_of_eqOn_dense

added theorem FirstOrder.Language.Hom.eq_of_eqOn_top

added theorem FirstOrder.Language.Hom.map_le_range

added theorem FirstOrder.Language.Hom.mem_range

added theorem FirstOrder.Language.Hom.mem_range_self

added def FirstOrder.Language.Hom.range

added theorem FirstOrder.Language.Hom.range_coe

added theorem FirstOrder.Language.Hom.range_comp

added theorem FirstOrder.Language.Hom.range_comp_le_range

added theorem FirstOrder.Language.Hom.range_eq_map

added theorem FirstOrder.Language.Hom.range_eq_top

added theorem FirstOrder.Language.Hom.range_id

added theorem FirstOrder.Language.Hom.range_le_iff_comap

added theorem FirstOrder.Language.Hom.subtype_comp_codRestrict

added theorem FirstOrder.Language.LHom.coe_substructureReduct

added theorem FirstOrder.Language.LHom.mem_substructureReduct

added def FirstOrder.Language.LHom.substructureReduct

added def FirstOrder.Language.Substructure.Simps.coe

added theorem FirstOrder.Language.Substructure.apply_coe_mem_map

added theorem FirstOrder.Language.Substructure.closed

added def FirstOrder.Language.Substructure.closure

added theorem FirstOrder.Language.Substructure.closure_empty

added theorem FirstOrder.Language.Substructure.closure_eq

added theorem FirstOrder.Language.Substructure.closure_eq_of_le

added theorem FirstOrder.Language.Substructure.closure_image

added theorem FirstOrder.Language.Substructure.closure_induction'

added theorem FirstOrder.Language.Substructure.closure_induction

added theorem FirstOrder.Language.Substructure.closure_le

added theorem FirstOrder.Language.Substructure.closure_mono

added theorem FirstOrder.Language.Substructure.closure_union

added theorem FirstOrder.Language.Substructure.closure_unionᵢ

added theorem FirstOrder.Language.Substructure.closure_univ

added theorem FirstOrder.Language.Substructure.closure_withConstants_eq

added theorem FirstOrder.Language.Substructure.coeSubtype

added theorem FirstOrder.Language.Substructure.coe_closure_eq_range_term_realize

added theorem FirstOrder.Language.Substructure.coe_copy

added theorem FirstOrder.Language.Substructure.coe_inclusion

added theorem FirstOrder.Language.Substructure.coe_inf

added theorem FirstOrder.Language.Substructure.coe_infᵢ

added theorem FirstOrder.Language.Substructure.coe_infₛ

added theorem FirstOrder.Language.Substructure.coe_top

added theorem FirstOrder.Language.Substructure.coe_topEquiv

added theorem FirstOrder.Language.Substructure.coe_withConstants

added def FirstOrder.Language.Substructure.comap

added theorem FirstOrder.Language.Substructure.comap_comap

added theorem FirstOrder.Language.Substructure.comap_id

added theorem FirstOrder.Language.Substructure.comap_inf

added theorem FirstOrder.Language.Substructure.comap_inf_map_of_injective

added theorem FirstOrder.Language.Substructure.comap_infᵢ

added theorem FirstOrder.Language.Substructure.comap_infᵢ_map_of_injective

added theorem FirstOrder.Language.Substructure.comap_injective_of_surjective

added theorem FirstOrder.Language.Substructure.comap_le_comap_iff_of_surjective

added theorem FirstOrder.Language.Substructure.comap_map_comap

added theorem FirstOrder.Language.Substructure.comap_map_eq_of_injective

added theorem FirstOrder.Language.Substructure.comap_strictMono_of_surjective

added theorem FirstOrder.Language.Substructure.comap_sup_map_of_injective

added theorem FirstOrder.Language.Substructure.comap_supᵢ_map_of_injective

added theorem FirstOrder.Language.Substructure.comap_surjective_of_injective

added theorem FirstOrder.Language.Substructure.comap_top

added theorem FirstOrder.Language.Substructure.constants_mem

added theorem FirstOrder.Language.Substructure.copy_eq

added theorem FirstOrder.Language.Substructure.dense_induction

added theorem FirstOrder.Language.Substructure.ext

added theorem FirstOrder.Language.Substructure.gc_map_comap

added def FirstOrder.Language.Substructure.gciMapComap

added def FirstOrder.Language.Substructure.giMapComap

added def FirstOrder.Language.Substructure.inclusion

added theorem FirstOrder.Language.Substructure.le_comap_map

added theorem FirstOrder.Language.Substructure.le_comap_of_map_le

added theorem FirstOrder.Language.Substructure.lift_card_closure_le

added theorem FirstOrder.Language.Substructure.lift_card_closure_le_card_term

added def FirstOrder.Language.Substructure.map

added theorem FirstOrder.Language.Substructure.map_bot

added theorem FirstOrder.Language.Substructure.map_closure

added theorem FirstOrder.Language.Substructure.map_comap_eq_of_surjective

added theorem FirstOrder.Language.Substructure.map_comap_le

added theorem FirstOrder.Language.Substructure.map_comap_map

added theorem FirstOrder.Language.Substructure.map_id

added theorem FirstOrder.Language.Substructure.map_inf_comap_of_surjective

added theorem FirstOrder.Language.Substructure.map_infᵢ_comap_of_surjective

added theorem FirstOrder.Language.Substructure.map_injective_of_injective

added theorem FirstOrder.Language.Substructure.map_le_iff_le_comap

added theorem FirstOrder.Language.Substructure.map_le_map_iff_of_injective

added theorem FirstOrder.Language.Substructure.map_le_of_le_comap

added theorem FirstOrder.Language.Substructure.map_map

added theorem FirstOrder.Language.Substructure.map_strictMono_of_injective

added theorem FirstOrder.Language.Substructure.map_sup

added theorem FirstOrder.Language.Substructure.map_sup_comap_of_surjective

added theorem FirstOrder.Language.Substructure.map_supᵢ

added theorem FirstOrder.Language.Substructure.map_supᵢ_comap_of_surjective

added theorem FirstOrder.Language.Substructure.map_surjective_of_surjective

added theorem FirstOrder.Language.Substructure.mem_carrier

added theorem FirstOrder.Language.Substructure.mem_closure

added theorem FirstOrder.Language.Substructure.mem_closure_iff_exists_term

added theorem FirstOrder.Language.Substructure.mem_comap

added theorem FirstOrder.Language.Substructure.mem_inf

added theorem FirstOrder.Language.Substructure.mem_infᵢ

added theorem FirstOrder.Language.Substructure.mem_infₛ

added theorem FirstOrder.Language.Substructure.mem_map

added theorem FirstOrder.Language.Substructure.mem_map_of_mem

added theorem FirstOrder.Language.Substructure.mem_top

added theorem FirstOrder.Language.Substructure.mem_withConstants

added theorem FirstOrder.Language.Substructure.monotone_comap

added theorem FirstOrder.Language.Substructure.monotone_map

added theorem FirstOrder.Language.Substructure.not_mem_of_not_mem_closure

added theorem FirstOrder.Language.Substructure.range_subtype

added theorem FirstOrder.Language.Substructure.reduct_withConstants

added theorem FirstOrder.Language.Substructure.subset_closure

added theorem FirstOrder.Language.Substructure.subset_closure_withConstants

added def FirstOrder.Language.Substructure.subtype

added def FirstOrder.Language.Substructure.topEquiv

added def FirstOrder.Language.Substructure.withConstants

added structure FirstOrder.Language.Substructure

added theorem FirstOrder.Language.Term.realize_mem

added theorem FirstOrder.Language.closedUnder_univ

added theorem Set.Countable.substructure_closure