instance OmegaCompletePartialOrder.instPartialOrderOption_quasiBorelSpaces {α : Type u_1} [OmegaCompletePartialOrder α] : PartialOrder (Option α)

Bottom-order on options: none is bottom, some is ordered pointwise.

Equations

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

noncomputable def OmegaCompletePartialOrder.firstSomeIndex {α : Type u_1} [OmegaCompletePartialOrder α] (c : Chain (Option α)) (h : ∃ (n : ℕ) (x : α), c n = some x) : ℕ

Pick any index where a chain hits some

Equations

• OmegaCompletePartialOrder.firstSomeIndex c h = Classical.choose h

noncomputable def OmegaCompletePartialOrder.firstSomeValue {α : Type u_1} [OmegaCompletePartialOrder α] (c : Chain (Option α)) (h : ∃ (n : ℕ) (x : α), c n = some x) : α

A witness that the chain hits some at firstSomeIndex

Equations

• OmegaCompletePartialOrder.firstSomeValue c h = Classical.choose ⋯

theorem OmegaCompletePartialOrder.firstSome_spec {α : Type u_1} [OmegaCompletePartialOrder α] (c : Chain (Option α)) (h : ∃ (n : ℕ) (x : α), c n = some x) : c (firstSomeIndex c h) = some (firstSomeValue c h)

noncomputable def OmegaCompletePartialOrder.tailChain {α : Type u_1} [OmegaCompletePartialOrder α] (c : Chain (Option α)) (h : ∃ (n : ℕ) (x : α), c n = some x) : Chain α

Chain of underlying values after the first some, padding with the first value

Equations

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

@[simp]

theorem OmegaCompletePartialOrder.tailChain_apply {α : Type u_1} [OmegaCompletePartialOrder α] (c : Chain (Option α)) (h : ∃ (n : ℕ) (x : α), c n = some x) (k : ℕ) : (tailChain c h) k = match c (firstSomeIndex c h + k) with | some x => x | none => firstSomeValue c h

noncomputable def OmegaCompletePartialOrder.optionωSup {α : Type u_1} [OmegaCompletePartialOrder α] (c : Chain (Option α)) : Option α

ω-supremum on Option α: either none for an all-bottom chain, or some of the ω-supremum of the tail of defined elements.

Equations

• OmegaCompletePartialOrder.optionωSup c = if h : ∃ (n : ℕ) (x : α), c n = some x then some (OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.tailChain c h)) else none

noncomputable instance OmegaCompletePartialOrder.instOption_quasiBorelSpaces {α : Type u_1} [OmegaCompletePartialOrder α] : OmegaCompletePartialOrder (Option α)

ω-supremum on Option α: either none for an all-bottom chain, or some of the ω-supremum of the tail of defined elements

Equations

• OmegaCompletePartialOrder.instOption_quasiBorelSpaces = { toPartialOrder := inferInstance, ωSup := OmegaCompletePartialOrder.optionωSup, le_ωSup := ⋯, ωSup_le := ⋯ }