Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-18 18:52 15444e1f

View on Github →

feat(model_theory/basic): more substructure API, including subtype, map, and comap (#7937) Defines first_order.language.embedding.of_injective, which bundles an injective hom in an algebraic language as an embedding Defines the induced L.Structure on an L.substructure Defines the embedding S.subtype from S : L.substructure M into M Defines substructure.map and substructure.comap and associated API including Galois insertions

Estimated changes

Modified src/model_theory/basic.lean

added theorem first_order.language.embedding.coe_fn_of_injective

added def first_order.language.embedding.of_injective

added theorem first_order.language.embedding.of_injective_to_hom

added theorem first_order.language.substructure.apply_coe_mem_map

added theorem first_order.language.substructure.closure_induction'

added theorem first_order.language.substructure.coe_subtype

added def first_order.language.substructure.comap

added theorem first_order.language.substructure.comap_comap

added theorem first_order.language.substructure.comap_id

added theorem first_order.language.substructure.comap_inf

added theorem first_order.language.substructure.comap_inf_map_of_injective

added theorem first_order.language.substructure.comap_infi

added theorem first_order.language.substructure.comap_infi_map_of_injective

added theorem first_order.language.substructure.comap_injective_of_surjective

added theorem first_order.language.substructure.comap_le_comap_iff_of_surjective

added theorem first_order.language.substructure.comap_map_comap

added theorem first_order.language.substructure.comap_map_eq_of_injective

added theorem first_order.language.substructure.comap_strict_mono_of_surjective

added theorem first_order.language.substructure.comap_sup_map_of_injective

added theorem first_order.language.substructure.comap_supr_map_of_injective

added theorem first_order.language.substructure.comap_surjective_of_injective

added theorem first_order.language.substructure.comap_top

added theorem first_order.language.substructure.gc_map_comap

added def first_order.language.substructure.gci_map_comap

added def first_order.language.substructure.gi_map_comap

added theorem first_order.language.substructure.le_comap_map

added theorem first_order.language.substructure.le_comap_of_map_le

added def first_order.language.substructure.map

added theorem first_order.language.substructure.map_bot

added theorem first_order.language.substructure.map_comap_eq_of_surjective

added theorem first_order.language.substructure.map_comap_le

added theorem first_order.language.substructure.map_comap_map

added theorem first_order.language.substructure.map_id

added theorem first_order.language.substructure.map_inf_comap_of_surjective

added theorem first_order.language.substructure.map_infi_comap_of_surjective

added theorem first_order.language.substructure.map_injective_of_injective

added theorem first_order.language.substructure.map_le_iff_le_comap

added theorem first_order.language.substructure.map_le_map_iff_of_injective

added theorem first_order.language.substructure.map_le_of_le_comap

added theorem first_order.language.substructure.map_map

added theorem first_order.language.substructure.map_strict_mono_of_injective

added theorem first_order.language.substructure.map_sup

added theorem first_order.language.substructure.map_sup_comap_of_surjective

added theorem first_order.language.substructure.map_supr

added theorem first_order.language.substructure.map_supr_comap_of_surjective

added theorem first_order.language.substructure.map_surjective_of_surjective

added theorem first_order.language.substructure.mem_comap

added theorem first_order.language.substructure.mem_map

added theorem first_order.language.substructure.mem_map_of_mem

added theorem first_order.language.substructure.monotone_comap

added theorem first_order.language.substructure.monotone_map

added def first_order.language.substructure.subtype