Companion.prelim

Section 2: Preliminaries

We show part of Tarski's theorem, namely that every monotone function on a complete lattice has a greatest fixed point. The basic definition of lattices are imported from an in progress formalization of order theory.

From Ord Require Export base preorder order adjunction jlat mlat lat clat.

Section Tarski.
Variables (A : clat) (f : A -> A).
Hypothesis (fP : monotone f).

Definition nu := \sup_(x | x <= f x) x.

Lemma nu_tarski x : x <= f x -> x <= nu.
Proof. move=> h. exact: supIc le_refl. Qed.

Lemma nu_postfix : nu <= f nu.
Proof.
apply: supEc => x le_x_fx. rewrite le_x_fx.
apply: mono. exact: nu_tarski.
Qed.

Lemma nu_prefix : f nu <= nu.
Proof. apply: supIc le_refl. by rewrite {1}nu_postfix. Qed.

Lemma nu_fp : f nu = nu.
Proof. apply: le_eq. exact: nu_prefix. exact: nu_postfix. Qed.
End Tarski.