Documentation

Mathlib.ModelTheory.ElementaryMaps

Elementary Maps Between First-Order Structures #

Main Definitions #

Main Results #

An elementary embedding of first-order structures is an embedding that commutes with the realizations of formulas.

Instances For

    An elementary embedding of first-order structures is an embedding that commutes with the realizations of formulas.

    Instances For

      An elementary embedding is also a first-order homomorphism.

      Instances For

        The identity elementary embedding from a structure to itself

        Instances For
          @[inline, reducible]

          The elementary diagram of an L-structure is the set of all sentences with parameters it satisfies.

          Instances For

            The Tarski-Vaught test for elementarity of an embedding.

            Bundles an embedding satisfying the Tarski-Vaught test as an elementary embedding.

            Instances For

              A first-order equivalence is also an elementary embedding.

              Instances For
                @[simp]

                A substructure is elementary when every formula applied to a tuple in the subtructure agrees with its value in the overall structure.

                Instances For

                  An elementary substructure is one in which every formula applied to a tuple in the subtructure agrees with its value in the overall structure.

                  Instances For

                    The natural embedding of an L.Substructure of M into M.

                    Instances For

                      The Tarski-Vaught test for elementarity of a substructure.

                      Bundles a substructure satisfying the Tarski-Vaught test as an elementary substructure.

                      Instances For