06 Order, lattices, ordered algebraic structures

DefinitionBirkhoff's representation theorem#

Birkhoff's Representation Theorem. Any finite distributive lattice can be embedded in a powerset lattice.

LatticeHom.birkhoffSet.{u_1} {α : Type u_1} [DistribLattice α] [Fintype α]
  [DecidablePred SupIrred] : LatticeHom α (Set { a // SupIrred a })
Sources
MathlibLatticeHom.birkhoffSet
Uses 2
Statement usesFinite set · Set

TheoremBourbaki–Witt theorem#

The Bourbaki-Witt Theorem: If α is a chain complete partial order and f : α → α is inflationary, then f has a fixed point

ChainCompletePartialOrder.nonempty_fixedPoints_of_inflationary.{u_1} {α : Type u_1}
  [ChainCompletePartialOrder α] {f : α → α} [Nonempty α] (le_map : ∀ (x : α), x ≤ f x) :
  (Function.fixedPoints f).Nonempty
Sources
MathlibChainCompletePartialOrder.nonempty_fixedPoints_of_inflationary
Uses 1
Statement usesFixed points

TheoremCantor's isomorphism theorem#

Any two countable dense, nonempty linear orders without endpoints are order isomorphic. This is also known as Cantor's isomorphism theorem.

Order.iso_of_countable_dense.{u_1, u_2} (α : Type u_1) (β : Type u_2) [LinearOrder α]
  [LinearOrder β] [Countable α] [DenselyOrdered α] [NoMinOrder α] [NoMaxOrder α] [Nonempty α]
  [Countable β] [DenselyOrdered β] [NoMinOrder β] [NoMaxOrder β] [Nonempty β] : Nonempty (α ≃o β)
Sources
MathlibOrder.iso_of_countable_dense
Uses 2
Statement usesNatural number
Proof usesFinite set

TheoremHahn embedding theorem#

Hahn embedding theorem

For a linearly ordered additive group M, there exists an injective OrderAddMonoidHom from M to Lex ℝ⟦FiniteArchimedeanClass M⟧ that sends each a : M to an element of the a-Archimedean class of the Hahn series.

hahnEmbedding_isOrderedAddMonoid.{u_1} (M : Type u_1) [AddCommGroup M] [LinearOrder M]
  [IsOrderedAddMonoid M] :
  ∃ f,
    Function.Injective ⇑f ∧
      ∀ (a : M),
        ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (f a)).orderTop
Sources
MathlibhahnEmbedding_isOrderedAddMonoid
Uses 8
Statement usesReal number
Proof usesAssociative algebra over a commutative ring · Characteristic zero · Completeness · Linear map · Normed vector space over a normed field · Ordered ring · Sum of subspaces

TheoremKleene fixed-point theorem#

Kleene's fixed point Theorem: The least fixed point in a complete lattice is the supremum of iterating a function on bottom arbitrary often.

fixedPoints.lfp_eq_sSup_iterate.{u} {α : Type u} [CompleteLattice α] (f : α →o α)
  (h : OmegaCompletePartialOrder.ωScottContinuous ⇑f) : OrderHom.lfp f = ⨆ n, (⇑f)^[n] ⊥
Sources
MathlibfixedPoints.lfp_eq_sSup_iterate
Uses 2
Statement usesNatural number
Proof usesFixed points

InstanceKnaster–Tarski theorem#

Knaster-Tarski Theorem: The fixed points of f form a complete lattice.

fixedPoints.completeLattice.{u} {α : Type u} [CompleteLattice α] (f : α →o α) :
  CompleteLattice ↑(Function.fixedPoints ⇑f)
Sources
MathlibfixedPoints.completeLattice
Uses 1
Statement usesFixed points

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.