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 #

A chain is a monotone sequence.

See the definition on page 114 of [Gun92].

Equations
Instances For
    Equations
    Equations
    Equations
    theorem OmegaCompletePartialOrder.Chain.isChain_range {α : Type u_2} [Preorder α] (c : Chain α) :
    IsChain (fun (x1 x2 : α) => x1 x2) (Set.range c)
    theorem OmegaCompletePartialOrder.Chain.directed {α : Type u_2} [Preorder α] (c : Chain α) :
    Directed (fun (x1 x2 : α) => x1 x2) c
    def OmegaCompletePartialOrder.Chain.map {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c : Chain α) (f : α →o β) :

    map function for Chain

    Equations
    Instances For
      @[simp]
      theorem OmegaCompletePartialOrder.Chain.map_coe {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c : Chain α) (f : α →o β) :
      (c.map f) = f c
      theorem OmegaCompletePartialOrder.Chain.mem_map {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c : Chain α) {f : α →o β} (x : α) :
      x cf x c.map f
      theorem OmegaCompletePartialOrder.Chain.exists_of_mem_map {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c : Chain α) {f : α →o β} {b : β} :
      b c.map fac, f a = b
      @[simp]
      theorem OmegaCompletePartialOrder.Chain.mem_map_iff {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c : Chain α) {f : α →o β} {b : β} :
      b c.map f ac, f a = b
      @[simp]
      theorem OmegaCompletePartialOrder.Chain.map_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [Preorder α] [Preorder β] [Preorder γ] (c : Chain α) {f : α →o β} (g : β →o γ) :
      (c.map f).map g = c.map (g.comp f)
      theorem OmegaCompletePartialOrder.Chain.map_le_map {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c : Chain α) {f g : α →o β} (h : f g) :
      c.map f c.map g
      def OmegaCompletePartialOrder.Chain.zip {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (c₀ : Chain α) (c₁ : Chain β) :
      Chain (α × β)

      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_2} {β : Type u_3} [Preorder α] [Preorder β] (c₀ : Chain α) (c₁ : Chain β) (n : ) :
        (c₀.zip c₁) n = (c₀ n, c₁ n)
        def OmegaCompletePartialOrder.Chain.pair {α : Type u_2} [Preorder α] (a b : α) (hab : a b) :

        An example of a Chain constructed from an ordered pair.

        Equations
        Instances For
          @[simp]
          theorem OmegaCompletePartialOrder.Chain.pair_zero {α : Type u_2} [Preorder α] (a b : α) (hab : a b) :
          (pair a b hab) 0 = a
          @[simp]
          theorem OmegaCompletePartialOrder.Chain.pair_succ {α : Type u_2} [Preorder α] (a b : α) (hab : a b) (n : ) :
          (pair a b hab) (n + 1) = b
          @[simp]
          theorem OmegaCompletePartialOrder.Chain.range_pair {α : Type u_2} [Preorder α] (a b : α) (hab : a b) :
          Set.range (pair a b hab) = {a, b}
          @[simp]
          theorem OmegaCompletePartialOrder.Chain.pair_zip_pair {α : Type u_2} {β : Type u_3} [Preorder α] [Preorder β] (a₁ a₂ : α) (b₁ b₂ : β) (ha : a₁ a₂) (hb : b₁ b₂) :
          (pair a₁ a₂ ha).zip (pair b₁ b₂ hb) = pair (a₁, b₁) (a₂, b₂)
          class OmegaCompletePartialOrder (α : Type u_6) extends PartialOrder α :
          Type u_6

          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 [Gun92].

          Instances
            @[reducible, inline]
            abbrev OmegaCompletePartialOrder.lift {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [PartialOrder β] (f : β →o α) (ωSup₀ : Chain ββ) (h : ∀ (x y : β), f x f yx y) (h' : ∀ (c : Chain β), f (ωSup₀ c) = ω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
              theorem OmegaCompletePartialOrder.le_ωSup_of_le {α : Type u_2} [OmegaCompletePartialOrder α] {c : Chain α} {x : α} (i : ) (h : x c i) :
              theorem OmegaCompletePartialOrder.ωSup_total {α : Type u_2} [OmegaCompletePartialOrder α] {c : Chain α} {x : α} (h : ∀ (i : ), c i x x c i) :
              theorem OmegaCompletePartialOrder.ωSup_le_ωSup_of_le {α : Type u_2} [OmegaCompletePartialOrder α] {c₀ c₁ : Chain α} (h : c₀ c₁) :
              ωSup c₀ ωSup c₁
              @[simp]
              theorem OmegaCompletePartialOrder.ωSup_le_iff {α : Type u_2} [OmegaCompletePartialOrder α] {c : Chain α} {x : α} :
              ωSup c x ∀ (i : ), c i x
              theorem OmegaCompletePartialOrder.ωSup_eq_of_isLUB {α : Type u_2} [OmegaCompletePartialOrder α] {c : Chain α} {a : α} (h : IsLUB (Set.range c) a) :
              a = ωSup c
              def OmegaCompletePartialOrder.subtype {α : Type u_6} [OmegaCompletePartialOrder α] (p : αProp) (hp : ∀ (c : Chain α), (∀ ic, p i)p (ωSup c)) :

              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 function f between ω-complete partial orders is ωScottContinuous if it is Scott continuous over chains.

                Equations
                Instances For
                  theorem OmegaCompletePartialOrder.ωScottContinuous.isLUB {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : αβ} {c : Chain α} (hf : ωScottContinuous f) :
                  IsLUB (Set.range (c.map { toFun := f, monotone' := })) (f (ωSup c))
                  theorem OmegaCompletePartialOrder.ωScottContinuous.map_ωSup {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : αβ} (hf : ωScottContinuous f) (c : Chain α) :
                  f (ωSup c) = ωSup (c.map { toFun := f, monotone' := })
                  theorem OmegaCompletePartialOrder.ωScottContinuous_iff_monotone_map_ωSup {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : αβ} :
                  ωScottContinuous f ∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })

                  ωScottContinuous f asserts that f is both monotone and distributes over ωSup.

                  theorem OmegaCompletePartialOrder.ωScottContinuous.of_monotone_map_ωSup {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : αβ} :
                  (∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf }))ωScottContinuous f

                  Alias of the reverse direction of OmegaCompletePartialOrder.ωScottContinuous_iff_monotone_map_ωSup.


                  ωScottContinuous f asserts that f is both monotone and distributes over ωSup.

                  theorem OmegaCompletePartialOrder.ωScottContinuous.monotone_map_ωSup {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f : αβ} :
                  ωScottContinuous f∃ (hf : Monotone f), ∀ (c : Chain α), f (ωSup c) = ωSup (c.map { toFun := f, monotone' := hf })

                  Alias of the forward direction of OmegaCompletePartialOrder.ωScottContinuous_iff_monotone_map_ωSup.


                  ωScottContinuous f asserts that f is both monotone and distributes over ωSup.

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

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

                  Equations
                  Instances For
                    theorem Part.ωSup_eq_some {α : Type u_2} {c : OmegaCompletePartialOrder.Chain (Part α)} {a : α} (h : some a c) :
                    theorem Part.ωSup_eq_none {α : Type u_2} {c : OmegaCompletePartialOrder.Chain (Part α)} (h : ¬∃ (a : α), some a c) :
                    instance instOmegaCompletePartialOrderForall {α : Type u_2} {β : αType u_6} [(a : α) → OmegaCompletePartialOrder (β a)] :
                    OmegaCompletePartialOrder ((a : α) → β a)
                    Equations
                    • One or more equations did not get rendered due to their size.
                    theorem OmegaCompletePartialOrder.ωScottContinuous.apply₂ {α : Type u_2} {γ : Type u_4} {β : αType u_6} [(x : α) → OmegaCompletePartialOrder (β x)] [OmegaCompletePartialOrder γ] {f : γ(x : α) → β x} (hf : ωScottContinuous f) (a : α) :
                    ωScottContinuous fun (x : γ) => f x a
                    theorem OmegaCompletePartialOrder.ωScottContinuous.of_apply₂ {α : Type u_2} {γ : Type u_4} {β : αType u_6} [(x : α) → OmegaCompletePartialOrder (β x)] [OmegaCompletePartialOrder γ] {f : γ(x : α) → β x} (hf : ∀ (a : α), ωScottContinuous fun (x : γ) => f x a) :
                    theorem OmegaCompletePartialOrder.ωScottContinuous_iff_apply₂ {α : Type u_2} {γ : Type u_4} {β : αType u_6} [(x : α) → OmegaCompletePartialOrder (β x)] [OmegaCompletePartialOrder γ] {f : γ(x : α) → β x} :
                    ωScottContinuous f ∀ (a : α), ωScottContinuous fun (x : γ) => f x a

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

                    Equations
                    Instances For
                      @[instance 100]

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

                      Equations
                      theorem CompleteLattice.ωScottContinuous.iSup {ι : Sort u_1} {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [CompleteLattice β] {f : ιαβ} (hf : ∀ (i : ι), OmegaCompletePartialOrder.ωScottContinuous (f i)) :

                      The ωSup operator for monotone functions.

                      Equations
                      Instances For
                        structure OmegaCompletePartialOrder.ContinuousHom (α : Type u_2) (β : Type u_3) [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] extends α →o β :
                        Type (max u_2 u_3)

                        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.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            Equations
                            @[simp]
                            theorem OmegaCompletePartialOrder.ContinuousHom.coe_mk {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →o β) (hf : ∀ (c : Chain α), f.toFun (ωSup c) = ωSup (c.map f)) :
                            { toOrderHom := f, map_ωSup' := hf } = f

                            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_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f g : α →𝒄 β} (h : f = g) (x : α) :
                              f x = g x
                              theorem OmegaCompletePartialOrder.ContinuousHom.congr_arg {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : α →𝒄 β) {x y : α} (h : x = y) :
                              f x = f y
                              theorem OmegaCompletePartialOrder.ContinuousHom.apply_mono {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] {f g : α →𝒄 β} {x y : α} (h₁ : f g) (h₂ : x y) :
                              f x g y
                              theorem OmegaCompletePartialOrder.ContinuousHom.ωSup_bind {α : Type u_2} [OmegaCompletePartialOrder α] {β γ : Type v} (c : Chain α) (f : α →o Part β) (g : α →o βPart γ) :
                              ωSup (c.map (f.partBind g)) = ωSup (c.map f) >>= ωSup (c.map g)
                              theorem OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.bind {α : Type u_2} [OmegaCompletePartialOrder α] {β γ : Type u_6} {f : αPart β} {g : αβPart γ} (hf : ωScottContinuous f) (hg : ωScottContinuous g) :
                              ωScottContinuous fun (x : α) => f x >>= g x
                              theorem OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.map {α : Type u_2} [OmegaCompletePartialOrder α] {β γ : Type u_6} {f : βγ} {g : αPart β} (hg : ωScottContinuous g) :
                              ωScottContinuous fun (x : α) => f <$> g x
                              theorem OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous.seq {α : Type u_2} [OmegaCompletePartialOrder α] {β γ : Type u_6} {f : αPart (βγ)} {g : αPart β} (hf : ωScottContinuous f) (hg : ωScottContinuous g) :
                              ωScottContinuous fun (x : α) => f x <*> g x
                              def OmegaCompletePartialOrder.ContinuousHom.copy {α : Type u_2} {β : Type u_3} [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.copy_apply {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f : αβ) (g : α →𝒄 β) (h : f = g) (a✝ : α) :
                                (copy f g h) a✝ = f a✝

                                The identity as a continuous function.

                                Equations
                                Instances For

                                  The composition of continuous functions.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem OmegaCompletePartialOrder.ContinuousHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] (f : β →𝒄 γ) (g : α →𝒄 β) (a✝ : α) :
                                    (f.comp g) a✝ = f (g a✝)
                                    theorem OmegaCompletePartialOrder.ContinuousHom.ext {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f g : α →𝒄 β) (h : ∀ (x : α), f x = g x) :
                                    f = g
                                    theorem OmegaCompletePartialOrder.ContinuousHom.coe_inj {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (f g : α →𝒄 β) (h : f = g) :
                                    f = g
                                    @[simp]
                                    theorem OmegaCompletePartialOrder.ContinuousHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] [OmegaCompletePartialOrder δ] (f : γ →𝒄 δ) (g : β →𝒄 γ) (h : α →𝒄 β) :
                                    f.comp (g.comp h) = (f.comp g).comp h
                                    @[simp]
                                    theorem OmegaCompletePartialOrder.ContinuousHom.coe_apply {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (a : α) (f : α →𝒄 β) :
                                    f a = f a

                                    Function.const is a continuous function.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem OmegaCompletePartialOrder.ContinuousHom.const_apply {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (x : β) (a✝ : α) :
                                      (const x) a✝ = x

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

                                      Equations
                                      Instances For
                                        @[simp]
                                        theorem OmegaCompletePartialOrder.ContinuousHom.forall_forall_merge {α : Type u_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c₀ : Chain (α →𝒄 β)) (c₁ : 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_2} {β : Type u_3} [OmegaCompletePartialOrder α] [OmegaCompletePartialOrder β] (c₀ : Chain (α →𝒄 β)) (c₁ : 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

                                          The application of continuous functions as a continuous function.

                                          Equations
                                          Instances For
                                            def OmegaCompletePartialOrder.ContinuousHom.flip {β : Type u_3} {γ : Type u_4} [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] {α : Type u_6} (f : αβ →𝒄 γ) :
                                            β →𝒄 αγ

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

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem OmegaCompletePartialOrder.ContinuousHom.flip_apply {β : Type u_3} {γ : Type u_4} [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder γ] {α : Type u_6} (f : αβ →𝒄 γ) (x : β) (y : α) :
                                              (flip f) x y = (f y) x
                                              noncomputable def OmegaCompletePartialOrder.ContinuousHom.bind {α : Type u_2} [OmegaCompletePartialOrder α] {β γ : Type v} (f : α →𝒄 Part β) (g : α →𝒄 βPart γ) :

                                              Part.bind as a continuous function.

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

                                                Part.map as a continuous function.

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem OmegaCompletePartialOrder.ContinuousHom.map_apply {α : Type u_2} [OmegaCompletePartialOrder α] {β γ : Type v} (f : βγ) (g : α →𝒄 Part β) (x : α) :
                                                  (map f g) x = Part.map f (g x)
                                                  noncomputable def OmegaCompletePartialOrder.ContinuousHom.seq {α : Type u_2} [OmegaCompletePartialOrder α] {β γ : 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
                                                    @[simp]
                                                    theorem OmegaCompletePartialOrder.ContinuousHom.seq_apply {α : Type u_2} [OmegaCompletePartialOrder α] {β γ : Type v} (f : α →𝒄 Part (βγ)) (g : α →𝒄 Part β) (x : α) :
                                                    (f.seq g) x = f x <*> g x
                                                    def OmegaCompletePartialOrder.fixedPoints.iterateChain {α : Type u_2} [OmegaCompletePartialOrder α] (f : α →o α) (x : α) (h : x f x) :

                                                    Iteration of a function on an initial element interpreted as a chain.

                                                    Equations
                                                    Instances For

                                                      The supremum of iterating a function on x arbitrary often is a fixed point

                                                      theorem OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_le_prefixedPoint {α : Type u_2} [OmegaCompletePartialOrder α] (f : α →𝒄 α) (x : α) (h : x f x) {a : α} (h_a : f a a) (h_x_le_a : x a) :
                                                      ωSup (iterateChain (↑f) x h) a

                                                      The supremum of iterating a function on x arbitrary often is smaller than any prefixed point.

                                                      A prefixed point is a value a with f a ≤ a.

                                                      theorem OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_le_fixedPoint {α : Type u_2} [OmegaCompletePartialOrder α] (f : α →𝒄 α) (x : α) (h : x f x) {a : α} (h_a : a Function.fixedPoints f) (h_x_le_a : x a) :
                                                      ωSup (iterateChain (↑f) x h) a

                                                      The supremum of iterating a function on x arbitrary often is smaller than any fixed point.