Commit 2022-02-07 11:17 00908913

View on Github →

chore(model_theory/*): Split up model_theory/basic (#11846) Splits model_theory/basic into separate files: basic, substructures, terms_and_formulas, definability, quotients Improves documentation throughout

Estimated changes

Modified src/model_theory/basic.lean

deleted def first_order.language.bd_not

deleted def first_order.language.bounded_formula.relabel

deleted inductive first_order.language.bounded_formula

deleted theorem first_order.language.closed_under.Inf

deleted theorem first_order.language.closed_under.inf

deleted theorem first_order.language.closed_under.inter

deleted def first_order.language.closed_under

deleted theorem first_order.language.closed_under_univ

deleted theorem first_order.language.definable_set.coe_bot

deleted theorem first_order.language.definable_set.coe_compl

deleted theorem first_order.language.definable_set.coe_inf

deleted theorem first_order.language.definable_set.coe_sup

deleted theorem first_order.language.definable_set.coe_top

deleted theorem first_order.language.definable_set.le_iff

deleted theorem first_order.language.definable_set.mem_compl

deleted theorem first_order.language.definable_set.mem_inf

deleted theorem first_order.language.definable_set.mem_sup

deleted theorem first_order.language.definable_set.mem_top

deleted theorem first_order.language.definable_set.not_mem_bot

deleted def first_order.language.definable_set

deleted theorem first_order.language.embedding.realize_term

deleted theorem first_order.language.equiv.realize_bounded_formula

deleted theorem first_order.language.equiv.realize_term

deleted def first_order.language.formula.equal

deleted def first_order.language.formula.graph

deleted def first_order.language.formula

deleted theorem first_order.language.fun_map_quotient_mk

deleted def first_order.language.hom.eq_locus

deleted theorem first_order.language.hom.eq_of_eq_on_dense

deleted theorem first_order.language.hom.eq_of_eq_on_top

deleted theorem first_order.language.hom.eq_on_closure

deleted theorem first_order.language.hom.realize_term

deleted theorem first_order.language.is_definable.compl

deleted theorem first_order.language.is_definable.inter

deleted theorem first_order.language.is_definable.sdiff

deleted theorem first_order.language.is_definable.union

deleted structure first_order.language.is_definable

deleted theorem first_order.language.is_definable_empty

deleted theorem first_order.language.is_definable_univ

deleted def first_order.language.realize_bounded_formula

deleted theorem first_order.language.realize_bounded_formula_relabel

deleted theorem first_order.language.realize_bounded_formula_top

deleted theorem first_order.language.realize_equal

deleted def first_order.language.realize_formula

deleted theorem first_order.language.realize_formula_equiv

deleted theorem first_order.language.realize_formula_relabel

deleted theorem first_order.language.realize_graph

deleted theorem first_order.language.realize_not

deleted def first_order.language.realize_sentence

deleted def first_order.language.realize_term

deleted theorem first_order.language.realize_term_quotient_mk

deleted theorem first_order.language.realize_term_relabel

deleted theorem first_order.language.realize_term_substructure

deleted def first_order.language.sentence

deleted theorem first_order.language.substructure.apply_coe_mem_map

deleted theorem first_order.language.substructure.closed

deleted def first_order.language.substructure.closure

deleted theorem first_order.language.substructure.closure_Union

deleted theorem first_order.language.substructure.closure_empty

deleted theorem first_order.language.substructure.closure_eq

deleted theorem first_order.language.substructure.closure_eq_of_le

deleted theorem first_order.language.substructure.closure_induction'

deleted theorem first_order.language.substructure.closure_induction

deleted theorem first_order.language.substructure.closure_le

deleted theorem first_order.language.substructure.closure_mono

deleted theorem first_order.language.substructure.closure_union

deleted theorem first_order.language.substructure.closure_univ

deleted theorem first_order.language.substructure.coe_Inf

deleted theorem first_order.language.substructure.coe_copy

deleted theorem first_order.language.substructure.coe_inf

deleted theorem first_order.language.substructure.coe_infi

deleted theorem first_order.language.substructure.coe_subtype

deleted theorem first_order.language.substructure.coe_top

deleted theorem first_order.language.substructure.coe_top_equiv

deleted def first_order.language.substructure.comap

deleted theorem first_order.language.substructure.comap_comap

deleted theorem first_order.language.substructure.comap_id

deleted theorem first_order.language.substructure.comap_inf

deleted theorem first_order.language.substructure.comap_inf_map_of_injective

deleted theorem first_order.language.substructure.comap_infi

deleted theorem first_order.language.substructure.comap_infi_map_of_injective

deleted theorem first_order.language.substructure.comap_injective_of_surjective

deleted theorem first_order.language.substructure.comap_le_comap_iff_of_surjective

deleted theorem first_order.language.substructure.comap_map_comap

deleted theorem first_order.language.substructure.comap_map_eq_of_injective

deleted theorem first_order.language.substructure.comap_strict_mono_of_surjective

deleted theorem first_order.language.substructure.comap_sup_map_of_injective

deleted theorem first_order.language.substructure.comap_supr_map_of_injective

deleted theorem first_order.language.substructure.comap_surjective_of_injective

deleted theorem first_order.language.substructure.comap_top

deleted theorem first_order.language.substructure.const_mem

deleted theorem first_order.language.substructure.copy_eq

deleted theorem first_order.language.substructure.dense_induction

deleted theorem first_order.language.substructure.ext

deleted theorem first_order.language.substructure.gc_map_comap

deleted def first_order.language.substructure.gci_map_comap

deleted def first_order.language.substructure.gi_map_comap

deleted theorem first_order.language.substructure.le_comap_map

deleted theorem first_order.language.substructure.le_comap_of_map_le

deleted def first_order.language.substructure.map

deleted theorem first_order.language.substructure.map_bot

deleted theorem first_order.language.substructure.map_comap_eq_of_surjective

deleted theorem first_order.language.substructure.map_comap_le

deleted theorem first_order.language.substructure.map_comap_map

deleted theorem first_order.language.substructure.map_id

deleted theorem first_order.language.substructure.map_inf_comap_of_surjective

deleted theorem first_order.language.substructure.map_infi_comap_of_surjective

deleted theorem first_order.language.substructure.map_injective_of_injective

deleted theorem first_order.language.substructure.map_le_iff_le_comap

deleted theorem first_order.language.substructure.map_le_map_iff_of_injective

deleted theorem first_order.language.substructure.map_le_of_le_comap

deleted theorem first_order.language.substructure.map_map

deleted theorem first_order.language.substructure.map_strict_mono_of_injective

deleted theorem first_order.language.substructure.map_sup

deleted theorem first_order.language.substructure.map_sup_comap_of_surjective

deleted theorem first_order.language.substructure.map_supr

deleted theorem first_order.language.substructure.map_supr_comap_of_surjective

deleted theorem first_order.language.substructure.map_surjective_of_surjective

deleted theorem first_order.language.substructure.mem_Inf

deleted theorem first_order.language.substructure.mem_carrier

deleted theorem first_order.language.substructure.mem_closure

deleted theorem first_order.language.substructure.mem_comap

deleted theorem first_order.language.substructure.mem_inf

deleted theorem first_order.language.substructure.mem_infi

deleted theorem first_order.language.substructure.mem_map

deleted theorem first_order.language.substructure.mem_map_of_mem

deleted theorem first_order.language.substructure.mem_top

deleted theorem first_order.language.substructure.monotone_comap

deleted theorem first_order.language.substructure.monotone_map

deleted theorem first_order.language.substructure.not_mem_of_not_mem_closure

deleted def first_order.language.substructure.simps.coe

deleted theorem first_order.language.substructure.subset_closure

deleted def first_order.language.substructure.subtype

deleted def first_order.language.substructure.top_equiv

deleted structure first_order.language.substructure

deleted def first_order.language.term.relabel

deleted inductive first_order.language.term

deleted def first_order.language.theory

Created src/model_theory/definability.lean

added theorem first_order.language.definable_set.coe_bot

added theorem first_order.language.definable_set.coe_compl

added theorem first_order.language.definable_set.coe_inf

added theorem first_order.language.definable_set.coe_sup

added theorem first_order.language.definable_set.coe_top

added theorem first_order.language.definable_set.le_iff

added theorem first_order.language.definable_set.mem_compl

added theorem first_order.language.definable_set.mem_inf

added theorem first_order.language.definable_set.mem_sup

added theorem first_order.language.definable_set.mem_top

added theorem first_order.language.definable_set.not_mem_bot

added def first_order.language.definable_set

added theorem first_order.language.is_definable.compl

added theorem first_order.language.is_definable.inter

added theorem first_order.language.is_definable.sdiff

added theorem first_order.language.is_definable.union

added structure first_order.language.is_definable

added theorem first_order.language.is_definable_empty

added theorem first_order.language.is_definable_univ

Modified src/model_theory/elementary_maps.lean

added theorem first_order.language.realize_bounded_formula_top

added theorem first_order.language.realize_term_substructure

Created src/model_theory/quotients.lean

added theorem first_order.language.fun_map_quotient_mk

added theorem first_order.language.realize_term_quotient_mk

Created src/model_theory/substructures.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.closed_under_univ

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.substructure.apply_coe_mem_map

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_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_subtype

added theorem first_order.language.substructure.coe_top

added theorem first_order.language.substructure.coe_top_equiv

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.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.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_Inf

added theorem first_order.language.substructure.mem_carrier

added theorem first_order.language.substructure.mem_closure

added theorem first_order.language.substructure.mem_comap

added theorem first_order.language.substructure.mem_inf

added theorem first_order.language.substructure.mem_infi

added theorem first_order.language.substructure.mem_map

added theorem first_order.language.substructure.mem_map_of_mem

added theorem first_order.language.substructure.mem_top

added theorem first_order.language.substructure.monotone_comap

added theorem first_order.language.substructure.monotone_map

added theorem first_order.language.substructure.not_mem_of_not_mem_closure

added def first_order.language.substructure.simps.coe

added theorem first_order.language.substructure.subset_closure

added def first_order.language.substructure.subtype

added def first_order.language.substructure.top_equiv

added structure first_order.language.substructure

Created src/model_theory/terms_and_formulas.lean

added def first_order.language.bd_not

added def first_order.language.bounded_formula.relabel

added inductive first_order.language.bounded_formula

added theorem first_order.language.embedding.realize_term

added theorem first_order.language.equiv.realize_bounded_formula

added theorem first_order.language.equiv.realize_term

added def first_order.language.formula.equal

added def first_order.language.formula.graph

added def first_order.language.formula

added theorem first_order.language.hom.realize_term

added def first_order.language.realize_bounded_formula

added theorem first_order.language.realize_bounded_formula_relabel

added theorem first_order.language.realize_equal

added def first_order.language.realize_formula

added theorem first_order.language.realize_formula_equiv

added theorem first_order.language.realize_formula_relabel

added theorem first_order.language.realize_graph

added theorem first_order.language.realize_not

added def first_order.language.realize_sentence

added def first_order.language.realize_term

added theorem first_order.language.realize_term_relabel

added def first_order.language.sentence

added def first_order.language.term.relabel

added inductive first_order.language.term

added def first_order.language.theory