Documentation

LeanPool.QuasiBorelSpaces.OmegaCompletePartialOrder.Chain.Sum

Chain utilities for coproducts of ωCPOs #

This file provides utilities for working with chains in sum types, which are used to construct the ωCPO instance for coproducts.

source
def OmegaCompletePartialOrder.Chain.Sum.inl {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] (c : Chain A) :
Chain (A ⊕ B)

Left injection for chains of sums.

Equations
Instances For
    source
    @[simp]
    theorem OmegaCompletePartialOrder.Chain.Sum.inl_coe {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] (c : Chain A) (n : ℕ) :
    (inl c) n = _root_.Sum.inl (c n)
    source
    def OmegaCompletePartialOrder.Chain.Sum.inr {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] (c : Chain B) :
    Chain (A ⊕ B)

    Right injection for chains of sums.

    Equations
    Instances For
      source
      @[simp]
      theorem OmegaCompletePartialOrder.Chain.Sum.inr_coe {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] (c : Chain B) (n : ℕ) :
      (inr c) n = _root_.Sum.inr (c n)
      source
      def OmegaCompletePartialOrder.Chain.Sum.projl {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] [hA : Inhabited A] (c : Chain (A ⊕ B)) :
      Chain A

      Projects left values out of a chain.

      Equations
      Instances For
        source
        @[simp]
        theorem OmegaCompletePartialOrder.Chain.Sum.projl_coe {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] [Inhabited A] (c : Chain (A ⊕ B)) (n : ℕ) :
        (projl c) n = Sum.elim id (fun (x : B) => default) (c n)
        source
        def OmegaCompletePartialOrder.Chain.Sum.swapOrderHom {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] :
        A ⊕ B →o B ⊕ A

        Swaps the two sides of an ordered sum.

        Equations
        Instances For
          source
          @[simp]
          theorem OmegaCompletePartialOrder.Chain.Sum.swapOrderHom_apply {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] (x : A ⊕ B) :
          swapOrderHom x = x.swap
          source
          def OmegaCompletePartialOrder.Chain.Sum.projr {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] [hB : Inhabited B] (c : Chain (A ⊕ B)) :
          Chain B

          Projects right values out of a chain.

          Equations
          Instances For
            source
            @[simp]
            theorem OmegaCompletePartialOrder.Chain.Sum.projr_coe {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] [Inhabited B] (c : Chain (A ⊕ B)) (n : ℕ) :
            (projr c) n = Sum.elim (fun (x : A) => default) id (c n)
            source
            def OmegaCompletePartialOrder.Chain.Sum.distrib {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] (c : Chain (A ⊕ B)) :
            Chain A ⊕ Chain B

            Splits a chain of sums into a sum of chains.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[simp]
              theorem OmegaCompletePartialOrder.Chain.Sum.distrib_inl {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] (c : Chain A) :
              distrib (inl c) = _root_.Sum.inl c
              source
              @[simp]
              theorem OmegaCompletePartialOrder.Chain.Sum.distrib_inr {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] (c : Chain B) :
              distrib (inr c) = _root_.Sum.inr c
              source
              theorem OmegaCompletePartialOrder.Chain.Sum.distrib_cases {A : Type u_1} {B : Type u_2} [Preorder A] [Preorder B] {p : Chain (A ⊕ B) → Prop} (inl : ∀ (c : Chain A), p (inl c)) (inr : ∀ (c : Chain B), p (inr c)) (c : Chain (A ⊕ B)) :
              p c