mathlib documentation

model_theory.bundled

Bundled First-Order Structures #

This file bundles types together with their first-order structure.

Main Definitions #

TODO #

@[protected, instance]

The equivalence relation on bundled L.Structures indicating that they are isomorphic.

Equations
structure first_order.language.Theory.Model {L : first_order.language} (T : L.Theory) :
Type (max u v (w+1))

The type of nonempty models of a first-order theory.

Instances for first_order.language.Theory.Model
def first_order.language.Theory.Model.of {L : first_order.language} (T : L.Theory) (M : Type w) [L.Structure M] [M T] [nonempty M] :

The object in the category of R-algebras associated to a type equipped with the appropriate typeclasses.

Equations
@[protected, instance]
def first_order.language.Theory.Model.equiv_induced {L : first_order.language} {T : L.Theory} {M : T.Model} {N : Type w'} (e : M N) :

Maps a bundled model along a bijection.

Equations
noncomputable def first_order.language.Theory.Model.shrink {L : first_order.language} {T : L.Theory} (M : T.Model) [small M] :

Shrinks a small model to a particular universe.

Equations

The reduct of any model of φ.on_Theory T is a model of T.

Equations
def first_order.language.Theory.model.bundled {L : first_order.language} {T : L.Theory} {M : Type w} [LM : L.Structure M] [ne : nonempty M] (h : M T) :

Bundles M ⊨ T as a T.Model.

Equations
@[simp]
theorem first_order.language.Theory.coe_of {L : first_order.language} {T : L.Theory} {M : Type w} [L.Structure M] [nonempty M] (h : M T) :

An elementary substructure of a bundled model as a bundled model.

Equations
Instances for first_order.language.elementary_substructure.to_Model