Documentation

Mathlib.ModelTheory.Order

Ordered First-Ordered Structures #

This file defines ordered first-order languages and structures, as well as their theories.

Main Definitions #

Main Results #

The language consisting of a single relation representing .

Instances For

    A language is ordered if it has a symbol representing .

    Instances

      Joins two terms t₁, t₂ in a formula representing t₁ ≤ t₂.

      Instances For

        Joins two terms t₁, t₂ in a formula representing t₁ < t₂.

        Instances For

          The language homomorphism sending the unique symbol of Language.order to in an ordered language.

          Instances For

            A sentence indicating that an order has no top element: $\forall x, \exists y, \neg y \le x$.

            Instances For

              A sentence indicating that an order has no bottom element: $\forall x, \exists y, \neg x \le y$.

              Instances For

                A sentence indicating that an order is dense: $\forall x, \forall y, x < y \to \exists z, x < z \wedge z < y$.

                Instances For

                  The theory of dense linear orders without endpoints.

                  Instances For
                    @[inline, reducible]

                    A structure is ordered if its language has a symbol whose interpretation is

                    Instances For