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 : α) :
↑(OrderHom.bind f 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

Instances For

    A chain is a monotone sequence.

    See the definition on page 114 of [gunter1992].

    Instances For
      theorem OmegaCompletePartialOrder.Chain.exists_of_mem_map {α : Type u} {β : Type v} [Preorder α] [Preorder β] (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} {b : β} :
      b OmegaCompletePartialOrder.Chain.map c fa, a c f a = b
      @[simp]
      theorem OmegaCompletePartialOrder.Chain.mem_map_iff {α : Type u} {β : Type v} [Preorder α] [Preorder β] (c : OmegaCompletePartialOrder.Chain α) {f : α →o β} {b : β} :

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

      Instances For
        @[simp]
        theorem OmegaCompletePartialOrder.Chain.zip_coe {α : Type u} {β : Type v} [Preorder α] [Preorder β] (c₀ : OmegaCompletePartialOrder.Chain α) (c₁ : OmegaCompletePartialOrder.Chain β) (n : ) :
        ↑(OmegaCompletePartialOrder.Chain.zip c₀ 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
          @[reducible]
          def 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 (OmegaCompletePartialOrder.Chain.map c 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 α.

          Instances For

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

            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).

              Instances For

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

                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 α.

                  Instances For
                    theorem Part.ωSup_eq_none {α : Type u} {c : OmegaCompletePartialOrder.Chain (Part α)} (h : ¬a, Part.some a c) :
                    Part.ωSup c = Part.none
                    instance Pi.instOmegaCompletePartialOrderForAll {α : Type u_1} {β : αType u_2} [(a : α) → OmegaCompletePartialOrder (β a)] :
                    OmegaCompletePartialOrder ((a : α) → β a)
                    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.

                    Instances For

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

                      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.

                      Instances For

                        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

                          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
                            @[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 FunLike instance.

                            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
                              @[simp]
                              theorem OmegaCompletePartialOrder.ContinuousHom.copy_apply {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : αβ) (g : α →𝒄 β) (h : f = g) :
                              ∀ (a : α), ↑(OmegaCompletePartialOrder.ContinuousHom.copy f g h) a = f a
                              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.

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

                                The identity as a continuous function.

                                Instances For

                                  The composition of continuous functions.

                                  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 : β →𝒄 γ) :
                                    OmegaCompletePartialOrder.ContinuousHom.comp f OmegaCompletePartialOrder.ContinuousHom.id = f
                                    @[simp]
                                    theorem OmegaCompletePartialOrder.ContinuousHom.id_comp {β : Type v} {γ : Type u_3} [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] (f : β →𝒄 γ) :
                                    OmegaCompletePartialOrder.ContinuousHom.comp OmegaCompletePartialOrder.ContinuousHom.id f = f
                                    @[simp]
                                    theorem OmegaCompletePartialOrder.ContinuousHom.coe_apply {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (a : α) (f : α →𝒄 β) :
                                    f a = f a

                                    Function.const is a continuous function.

                                    Instances For
                                      @[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.

                                      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.

                                        Instances For
                                          @[simp]
                                          theorem OmegaCompletePartialOrder.ContinuousHom.Prod.apply_apply {α : Type u} {β : Type v} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : (α →𝒄 β) × α) :
                                          OmegaCompletePartialOrder.ContinuousHom.Prod.apply f = f.fst f.snd

                                          The application of continuous functions as a continuous function.

                                          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.

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

                                              Part.bind as a continuous function.

                                              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.

                                                Instances For
                                                  @[simp]
                                                  theorem OmegaCompletePartialOrder.ContinuousHom.seq_apply {α : Type u} [OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : α →𝒄 Part (βγ)) (g : α →𝒄 Part β) (x : α) :
                                                  ↑(OmegaCompletePartialOrder.ContinuousHom.seq f g) x = Seq.seq (f x) fun x => g x
                                                  noncomputable def OmegaCompletePartialOrder.ContinuousHom.seq {α : Type u} [OmegaCompletePartialOrder α] {β : Type v} {γ : Type v} (f : α →𝒄 Part (βγ)) (g : α →𝒄 Part β) :

                                                  Part.seq as a continuous function.

                                                  Instances For