class OmegaCompletePartialOrderBi (α : Type) [instP : OmegaCompletePartialOrder α] [instD : OmegaCompletePartialOrder αᵒᵈ] : Prop

• preorder_eq : OrderDual.instPartialOrder α = OmegaCompletePartialOrder.toPartialOrder

instance CompleteLattice.instOmegaCompletePartialOrderBi (α : Type) [CompleteLattice α] : OmegaCompletePartialOrderBi α

@[reducible, inline]

abbrev OmegaCompletePartialOrderCo (α : Type) : Type

Equations

• OmegaCompletePartialOrderCo α = OmegaCompletePartialOrder αᵒᵈ

structure OrderDualHom (α β : Type) [Preorder α] [Preorder β] : Type

• toFun : α → β
• antitone' : Antitone self.toFun

instance instDFunLikeOrderDualHom {α β : Type} [Preorder α] [Preorder β] : DFunLike (OrderDualHom α β) α fun (x : α) => β

Equations

• instDFunLikeOrderDualHom = { coe := OrderDualHom.toFun, coe_injective' := ⋯ }

instance instPreorderOrderDualHom {α β : Type} [Preorder α] [Preorder β] : Preorder (OrderDualHom α β)

Equations

• instPreorderOrderDualHom = Preorder.lift OrderDualHom.toFun

def OrderDualHom.anti {α β : Type} [Preorder α] [Preorder β] (f : OrderDualHom α β) : Antitone ⇑f

Equations

• ⋯ = ⋯

def Cochain (α : Type) [Preorder α] : Type

Equations

• Cochain α = OrderDualHom ℕ α

instance instDFunLikeCochainNat {α : Type} [Preorder α] : DFunLike (Cochain α) ℕ fun (x : ℕ) => α

Equations

• instDFunLikeCochainNat = { coe := OrderDualHom.toFun, coe_injective' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrderBi.le_iff {α : Type} [instA : OmegaCompletePartialOrder α] [instB : OmegaCompletePartialOrder αᵒᵈ] [instBi : OmegaCompletePartialOrderBi α] {a b : α} : a ≤ b ↔ b ≤ a

def Cochain.toChain {α : Type} [instA : OmegaCompletePartialOrder α] [instB : OmegaCompletePartialOrder αᵒᵈ] [instBi : OmegaCompletePartialOrderBi α] (c : Cochain α) : OmegaCompletePartialOrder.Chain αᵒᵈ

Equations

• c.toChain = { toFun := ⇑c, monotone' := ⋯ }

def OmegaCompletePartialOrderBi.ωInf {α : Type} [instA : OmegaCompletePartialOrder α] [instB : OmegaCompletePartialOrder αᵒᵈ] [instBi : OmegaCompletePartialOrderBi α] (c : Cochain α) : α

Equations

• OmegaCompletePartialOrderBi.ωInf c = OmegaCompletePartialOrder.ωSup c.toChain

theorem OmegaCompletePartialOrderBi.le_ωInf {α : Type} [instA : OmegaCompletePartialOrder α] [instB : OmegaCompletePartialOrder αᵒᵈ] [instBi : OmegaCompletePartialOrderBi α] (c : Cochain α) (x : α) (h : ∀ (i : ℕ), x ≤ c i) : x ≤ ωInf c

theorem OmegaCompletePartialOrderBi.ωInf_le {α : Type} [instA : OmegaCompletePartialOrder α] [instB : OmegaCompletePartialOrder αᵒᵈ] [instBi : OmegaCompletePartialOrderBi α] (c : Cochain α) (i : ℕ) : ωInf c ≤ c i

def OmegaCompletePartialOrderBi.ωScottCocontinuous {α : Type u_1} {β : Type u_2} [OmegaCompletePartialOrder αᵒᵈ] [OmegaCompletePartialOrder βᵒᵈ] (f : α → β) : Prop

Equations

• OmegaCompletePartialOrderBi.ωScottCocontinuous f = OmegaCompletePartialOrder.ωScottContinuous f

def OmegaCompletePartialOrderBi.ωScottBicontinuous {α : Type} [instA : OmegaCompletePartialOrder α] [instB : OmegaCompletePartialOrder αᵒᵈ] {β : Type} [OmegaCompletePartialOrder β] [OmegaCompletePartialOrder βᵒᵈ] [OmegaCompletePartialOrderBi β] (f : α → β) : Prop

Equations

• OmegaCompletePartialOrderBi.ωScottBicontinuous f = (OmegaCompletePartialOrder.ωScottContinuous f ∧ OmegaCompletePartialOrderBi.ωScottCocontinuous f)