Documentation

Mathlib.Order.OmegaCompletePartialOrder

Omega Complete Partial Orders #

An omega-complete partial order is a partial order with a supremum operation on increasing sequences indexed by natural numbers (which we call ωSup). In this sense, it is strictly weaker than join complete semi-lattices as only ω-sized totally ordered sets have a supremum.

The concept of an omega-complete partial order (ωCPO) is useful for the formalization of the semantics of programming languages. Its notion of supremum helps define the meaning of recursive procedures.

Main definitions #

Instances of OmegaCompletePartialOrder #

References #

@[simp]
theorem OrderHom.bind_coe {α : Type u_1} [Preorder α] {β : Type u_4} {γ : Type u_4} (f : α →o Part β) (g : α →o βPart γ) (x : α) :
(f.bind g) x = f x >>= g x
def OrderHom.bind {α : Type u_1} [Preorder α] {β : Type u_4} {γ : Type u_4} (f : α →o Part β) (g : α →o βPart γ) :
α →o Part γ

Part.bind as a monotone function

Equations
  • f.bind g = { toFun := fun (x : α) => f x >>= g x, monotone' := }
Instances For

    A chain is a monotone sequence.

    See the definition on page 114 of [gunter1992].

    Equations
    Instances For
      Equations
      Equations
      • OmegaCompletePartialOrder.Chain.instCoeFunForallNat = { coe := DFunLike.coe }
      Equations
      • OmegaCompletePartialOrder.Chain.instInhabited = { default := { toFun := default, monotone' := } }
      Equations
      • OmegaCompletePartialOrder.Chain.instMembership = { mem := fun (a : α) (c : →o α) => ∃ (i : ), a = c i }
      Equations
      theorem OmegaCompletePartialOrder.Chain.directed {α : Type u} [Preorder α] (c : OmegaCompletePartialOrder.Chain α) :
      Directed (fun (x x_1 : α) => x x_1) c

      map function for Chain

      Equations
      • c.map f = f.comp c
      Instances For
        @[simp]
        theorem OmegaCompletePartialOrder.Chain.map_coe {α : Type u} {β : Type v} [Preorder α] [Preorder β] (c : OmegaCompletePartialOrder.Chain α) (f : α →o β) :
        (c.map f) = f c
        theorem OmegaCompletePartialOrder.Chain.mem_map {α : Type u} {β : Type v} [Preorder α] [Preorder β] (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} (x : α) :
        x cf x c.map f
        theorem OmegaCompletePartialOrder.Chain.exists_of_mem_map {α : Type u} {β : Type v} [Preorder α] [Preorder β] (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} {b : β} :
        b c.map fac, f a = b
        @[simp]
        theorem OmegaCompletePartialOrder.Chain.mem_map_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} {b : β} :
        b c.map f ac, f a = b
        @[simp]
        theorem OmegaCompletePartialOrder.Chain.map_id {α : Type u} [Preorder α] (c : OmegaCompletePartialOrder.Chain α) :
        c.map OrderHom.id = c
        theorem OmegaCompletePartialOrder.Chain.map_comp {α : Type u} {β : Type v} {γ : Type u_1} [Preorder α] [Preorder β] [Preorder γ] (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} (g : β →o γ) :
        (c.map f).map g = c.map (g.comp f)
        theorem OmegaCompletePartialOrder.Chain.map_le_map {α : Type u} {β : Type v} [Preorder α] [Preorder β] (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} {g : α →o β} (h : f g) :
        c.map f c.map g

        OmegaCompletePartialOrder.Chain.zip pairs up the elements of two chains that have the same index.

        Equations
        Instances For
          @[simp]
          theorem OmegaCompletePartialOrder.Chain.zip_coe {α : Type u} {β : Type v} [Preorder α] [Preorder β] (c₀ : OmegaCompletePartialOrder.Chain α) (c₁ : OmegaCompletePartialOrder.Chain β) (n : ) :
          (c₀.zip c₁) n = (c₀ n, c₁ n)
          class OmegaCompletePartialOrder (α : Type u_1) extends PartialOrder :
          Type u_1

          An omega-complete partial order is a partial order with a supremum operation on increasing sequences indexed by natural numbers (which we call ωSup). In this sense, it is strictly weaker than join complete semi-lattices as only ω-sized totally ordered sets have a supremum.

          See the definition on page 114 of [gunter1992].

          Instances

            ωSup is an upper bound of the increasing sequence

            ωSup is a lower bound of the set of upper bounds of the increasing sequence

            @[reducible, inline]
            abbrev OmegaCompletePartialOrder.lift {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [PartialOrder β] (f : β →o α) (ωSup₀ : OmegaCompletePartialOrder.Chain ββ) (h : ∀ (x y : β), f x f yx y) (h' : ∀ (c : OmegaCompletePartialOrder.Chain β), f (ωSup₀ c) = OmegaCompletePartialOrder.ωSup (c.map f)) :

            Transfer an OmegaCompletePartialOrder on β to an OmegaCompletePartialOrder on α using a strictly monotone function f : β →o α, a definition of ωSup and a proof that f is continuous with regard to the provided ωSup and the ωCPO on α.

            Equations
            Instances For

              A subset p : α → Prop of the type closed under ωSup induces an OmegaCompletePartialOrder on the subtype {a : α // p a}.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                A monotone function f : α →o β is continuous if it distributes over ωSup.

                In order to distinguish it from the (more commonly used) continuity from topology (see Mathlib/Topology/Basic.lean), the present definition is often referred to as "Scott-continuity" (referring to Dana Scott). It corresponds to continuity in Scott topological spaces (not defined here).

                Equations
                Instances For

                  Continuous' f asserts that f is both monotone and continuous.

                  Equations
                  Instances For
                    theorem Part.eq_of_chain {α : Type u} {c : OmegaCompletePartialOrder.Chain (Part α)} {a : α} {b : α} (ha : Part.some a c) (hb : Part.some b c) :
                    a = b
                    noncomputable def Part.ωSup {α : Type u} (c : OmegaCompletePartialOrder.Chain (Part α)) :
                    Part α

                    The (noncomputable) ωSup definition for the ω-CPO structure on Part α.

                    Equations
                    Instances For
                      theorem Part.ωSup_eq_none {α : Type u} {c : OmegaCompletePartialOrder.Chain (Part α)} (h : ¬∃ (a : α), Part.some a c) :
                      Part.ωSup c = Part.none
                      Equations
                      instance Pi.instOmegaCompletePartialOrderForall {α : Type u_1} {β : αType u_2} [(a : α) → OmegaCompletePartialOrder (β a)] :
                      OmegaCompletePartialOrder ((a : α) → β a)
                      Equations
                      • One or more equations did not get rendered due to their size.
                      theorem Pi.OmegaCompletePartialOrder.flip₁_continuous' {α : Type u_1} {β : αType u_2} {γ : Type u_3} [(x : α) → OmegaCompletePartialOrder (β x)] [OmegaCompletePartialOrder γ] (f : (x : α) → γβ x) (a : α) (hf : OmegaCompletePartialOrder.Continuous' fun (x : γ) (y : α) => f y x) :
                      theorem Pi.OmegaCompletePartialOrder.flip₂_continuous' {α : Type u_1} {β : αType u_2} {γ : Type u_3} [(x : α) → OmegaCompletePartialOrder (β x)] [OmegaCompletePartialOrder γ] (f : γ(x : α) → β x) (hf : ∀ (x : α), OmegaCompletePartialOrder.Continuous' fun (g : γ) => f g x) :

                      The supremum of a chain in the product ω-CPO.

                      Equations
                      Instances For
                        Equations
                        @[instance 100]

                        Any complete lattice has an ω-CPO structure where the countable supremum is a special case of arbitrary suprema.

                        Equations
                        theorem CompleteLattice.iSup_continuous {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [CompleteLattice β] {ι : Sort u_1} {f : ια →o β} (h : ∀ (i : ι), OmegaCompletePartialOrder.Continuous (f i)) :

                        The ωSup operator for monotone functions.

                        Equations
                        Instances For
                          Equations
                          • OmegaCompletePartialOrder.OrderHom.omegaCompletePartialOrder = OmegaCompletePartialOrder.lift OrderHom.coeFnHom OmegaCompletePartialOrder.OrderHom.ωSup

                          A monotone function on ω-continuous partial orders is said to be continuous if for every chain c : chain α, f (⊔ i, c i) = ⊔ i, f (c i). This is just the bundled version of OrderHom.continuous.

                          Instances For

                            The underlying function of a ContinuousHom is continuous, i.e. it preserves ωSup

                            A monotone function on ω-continuous partial orders is said to be continuous if for every chain c : chain α, f (⊔ i, c i) = ⊔ i, f (c i). This is just the bundled version of OrderHom.continuous.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              Equations
                              @[simp]
                              theorem OmegaCompletePartialOrder.ContinuousHom.coe_mk {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →o β) (hf : OmegaCompletePartialOrder.Continuous f) :
                              { toOrderHom := f, cont := hf } = f
                              @[simp]

                              See Note [custom simps projection]. We specify this explicitly because we don't have a DFunLike instance.

                              Equations
                              Instances For
                                theorem OmegaCompletePartialOrder.ContinuousHom.congr_fun {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α →𝒄 β} {g : α →𝒄 β} (h : f = g) (x : α) :
                                f x = g x
                                theorem OmegaCompletePartialOrder.ContinuousHom.congr_arg {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →𝒄 β) {x : α} {y : α} (h : x = y) :
                                f x = f y
                                theorem OmegaCompletePartialOrder.ContinuousHom.apply_mono {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : α →𝒄 β} {g : α →𝒄 β} {x : α} {y : α} (h₁ : f g) (h₂ : x y) :
                                f x g y
                                theorem OmegaCompletePartialOrder.ContinuousHom.seq_continuous' {α : Type u} [OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : αPart (βγ)) (g : αPart β) (hf : OmegaCompletePartialOrder.Continuous' f) (hg : OmegaCompletePartialOrder.Continuous' g) :
                                OmegaCompletePartialOrder.Continuous' fun (x : α) => Seq.seq (f x) fun (x_1 : Unit) => g x
                                @[simp]
                                theorem OmegaCompletePartialOrder.ContinuousHom.copy_apply {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : αβ) (g : α →𝒄 β) (h : f = g) :
                                def OmegaCompletePartialOrder.ContinuousHom.copy {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : αβ) (g : α →𝒄 β) (h : f = g) :
                                α →𝒄 β

                                Construct a continuous function from a bare function, a continuous function, and a proof that they are equal.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem OmegaCompletePartialOrder.ContinuousHom.id_apply {α : Type u} [OmegaCompletePartialOrder α] (a : α) :
                                  OmegaCompletePartialOrder.ContinuousHom.id a = a

                                  The identity as a continuous function.

                                  Equations
                                  • OmegaCompletePartialOrder.ContinuousHom.id = { toOrderHom := OrderHom.id, cont := }
                                  Instances For
                                    @[simp]
                                    theorem OmegaCompletePartialOrder.ContinuousHom.comp_apply {α : Type u} {β : Type v} {γ : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] (f : β →𝒄 γ) (g : α →𝒄 β) :
                                    ∀ (a : α), (f.comp g) a = f (g a)

                                    The composition of continuous functions.

                                    Equations
                                    • f.comp g = { toOrderHom := f.comp g.toOrderHom, cont := }
                                    Instances For
                                      theorem OmegaCompletePartialOrder.ContinuousHom.ext {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →𝒄 β) (g : α →𝒄 β) (h : ∀ (x : α), f x = g x) :
                                      f = g
                                      theorem OmegaCompletePartialOrder.ContinuousHom.coe_inj {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →𝒄 β) (g : α →𝒄 β) (h : f = g) :
                                      f = g
                                      @[simp]
                                      theorem OmegaCompletePartialOrder.ContinuousHom.comp_id {β : Type v} {γ : Type u_3} [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] (f : β →𝒄 γ) :
                                      f.comp OmegaCompletePartialOrder.ContinuousHom.id = f
                                      @[simp]
                                      theorem OmegaCompletePartialOrder.ContinuousHom.id_comp {β : Type v} {γ : Type u_3} [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] (f : β →𝒄 γ) :
                                      OmegaCompletePartialOrder.ContinuousHom.id.comp f = f
                                      @[simp]
                                      theorem OmegaCompletePartialOrder.ContinuousHom.comp_assoc {α : Type u} {β : Type v} {γ : Type u_3} {φ : Type u_4} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] [OmegaCompletePartialOrder φ] (f : γ →𝒄 φ) (g : β →𝒄 γ) (h : α →𝒄 β) :
                                      f.comp (g.comp h) = (f.comp g).comp h
                                      @[simp]

                                      Function.const is a continuous function.

                                      Equations
                                      Instances For
                                        Equations
                                        @[simp]
                                        theorem OmegaCompletePartialOrder.ContinuousHom.toMono_coe {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →𝒄 β) :
                                        OmegaCompletePartialOrder.ContinuousHom.toMono f = f

                                        The map from continuous functions to monotone functions is itself a monotone function.

                                        Equations
                                        • OmegaCompletePartialOrder.ContinuousHom.toMono = { toFun := fun (f : α →𝒄 β) => f, monotone' := }
                                        Instances For
                                          @[simp]
                                          theorem OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c₀ : OmegaCompletePartialOrder.Chain (α →𝒄 β)) (c₁ : OmegaCompletePartialOrder.Chain α) (z : β) :
                                          (∀ (i j : ), (c₀ i) (c₁ j) z) ∀ (i : ), (c₀ i) (c₁ i) z

                                          When proving that a chain of applications is below a bound z, it suffices to consider the functions and values being selected from the same index in the chains.

                                          This lemma is more specific than necessary, i.e. c₀ only needs to be a chain of monotone functions, but it is only used with continuous functions.

                                          @[simp]
                                          theorem OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge' {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c₀ : OmegaCompletePartialOrder.Chain (α →𝒄 β)) (c₁ : OmegaCompletePartialOrder.Chain α) (z : β) :
                                          (∀ (j i : ), (c₀ i) (c₁ j) z) ∀ (i : ), (c₀ i) (c₁ i) z

                                          The ωSup operator for continuous functions, which takes the pointwise countable supremum of the functions in the ω-chain.

                                          Equations
                                          Instances For
                                            Equations
                                            • OmegaCompletePartialOrder.ContinuousHom.inst = OmegaCompletePartialOrder.lift OmegaCompletePartialOrder.ContinuousHom.toMono OmegaCompletePartialOrder.ContinuousHom.ωSup
                                            @[simp]
                                            theorem OmegaCompletePartialOrder.ContinuousHom.Prod.apply_apply {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : (α →𝒄 β) × α) :
                                            OmegaCompletePartialOrder.ContinuousHom.Prod.apply f = f.1 f.2

                                            The application of continuous functions as a continuous function.

                                            Equations
                                            • OmegaCompletePartialOrder.ContinuousHom.Prod.apply = { toFun := fun (f : (α →𝒄 β) × α) => f.1 f.2, monotone' := , cont := }
                                            Instances For
                                              @[simp]
                                              theorem OmegaCompletePartialOrder.ContinuousHom.flip_apply {β : Type v} {γ : Type u_3} [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] {α : Type u_5} (f : αβ →𝒄 γ) (x : β) (y : α) :
                                              def OmegaCompletePartialOrder.ContinuousHom.flip {β : Type v} {γ : Type u_3} [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] {α : Type u_5} (f : αβ →𝒄 γ) :
                                              β →𝒄 αγ

                                              A family of continuous functions yields a continuous family of functions.

                                              Equations
                                              Instances For
                                                @[simp]
                                                theorem OmegaCompletePartialOrder.ContinuousHom.bind_apply {α : Type u} [OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : α →𝒄 Part β) (g : α →𝒄 βPart γ) (x : α) :
                                                (f.bind g) x = f x >>= g x
                                                noncomputable def OmegaCompletePartialOrder.ContinuousHom.bind {α : Type u} [OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : α →𝒄 Part β) (g : α →𝒄 βPart γ) :

                                                Part.bind as a continuous function.

                                                Equations
                                                • f.bind g = { toOrderHom := (f).bind g.toOrderHom, cont := }
                                                Instances For
                                                  @[simp]
                                                  theorem OmegaCompletePartialOrder.ContinuousHom.map_apply {α : Type u} [OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : βγ) (g : α →𝒄 Part β) (x : α) :
                                                  noncomputable def OmegaCompletePartialOrder.ContinuousHom.map {α : Type u} [OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : βγ) (g : α →𝒄 Part β) :

                                                  Part.map as a continuous function.

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    @[simp]
                                                    theorem OmegaCompletePartialOrder.ContinuousHom.seq_apply {α : Type u} [OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : α →𝒄 Part (βγ)) (g : α →𝒄 Part β) (x : α) :
                                                    (f.seq g) x = Seq.seq (f x) fun (x_1 : Unit) => g x
                                                    noncomputable def OmegaCompletePartialOrder.ContinuousHom.seq {α : Type u} [OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : α →𝒄 Part (βγ)) (g : α →𝒄 Part β) :

                                                    Part.seq as a continuous function.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For