mathlib3 documentation

model_theory.order

Ordered First-Ordered Structures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file defines ordered first-order languages and structures, as well as their theories.

Main Definitions #

Main Results #

@[class]

A language is ordered if it has a symbol representing .

Instances of this typeclass
Instances of other typeclasses for first_order.language.is_ordered
  • first_order.language.is_ordered.has_sizeof_inst
def first_order.language.term.le {L : first_order.language} {α : Type w} {n : } [L.is_ordered] (t₁ t₂ : L.term fin n)) :

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

Equations
def first_order.language.term.lt {L : first_order.language} {α : Type w} {n : } [L.is_ordered] (t₁ t₂ : L.term fin n)) :

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

Equations

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

Equations
Instances for first_order.language.order_Lhom

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

Equations

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

Equations

The theory of dense linear orders without endpoints.

Equations
Instances for first_order.language.DLO
@[reducible]

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

@[simp]
theorem first_order.language.term.realize_le {L : first_order.language} {α : Type w} {M : Type w'} {n : } [L.is_ordered] [L.Structure M] [has_le M] [L.ordered_structure M] {t₁ t₂ : L.term fin n)} {v : α M} {xs : fin n M} :
@[simp]
theorem first_order.language.term.realize_lt {L : first_order.language} {α : Type w} {M : Type w'} {n : } [L.is_ordered] [L.Structure M] [preorder M] [L.ordered_structure M] {t₁ t₂ : L.term fin n)} {v : α M} {xs : fin n M} :