def OmegaCompletePartialOrder.Chain.Option.none {A : Type u_1} [Preorder A] : Chain (Option A)

A chain of nones.

Equations

• OmegaCompletePartialOrder.Chain.Option.none = { toFun := fun (x : ℕ) => none, monotone' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.Chain.Option.none_coe {A : Type u_1} [Preorder A] {n : ℕ} : none n = _root_.Option.none

def OmegaCompletePartialOrder.Chain.Option.some {A : Type u_1} [Preorder A] (i : ℕ) (c : Chain A) : Chain (Option A)

Lifts a chain of values to a chain of somes, with the specified number of leading nones.

Equations

• OmegaCompletePartialOrder.Chain.Option.some i c = { toFun := fun (n : ℕ) => if n < i then none else some (c (n - i)), monotone' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.Chain.Option.some_coe {A : Type u_1} [Preorder A] (i n : ℕ) (c : Chain A) : (some i c) n = if n < i then _root_.Option.none else _root_.Option.some (c (n - i))

noncomputable def OmegaCompletePartialOrder.Chain.Option.project {A : Type u_1} [Preorder A] (c : Chain (Option A)) (h : ∃ (n : ℕ), (c n).isSome = true) : Chain A

Given a proof that a Chain contains a some value, we can construct a Chain that only contains the some values.

Equations

• OmegaCompletePartialOrder.Chain.Option.project c h = { toFun := fun (n : ℕ) => (c (Nat.find h + n)).getD ⋯.some, monotone' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.Chain.Option.project_coe {A : Type u_1} [Preorder A] (c : Chain (Option A)) (h : ∃ (n : ℕ), (c n).isSome = true) (n : ℕ) : (project c h) n = have this := ⋯; (c (Nat.find h + n)).getD this.some

noncomputable def OmegaCompletePartialOrder.Chain.Option.distrib {A : Type u_1} [Preorder A] (c : Chain (Option A)) : Option (Chain A)

Turns a Chain of Options into an equivalent Optional Chain.

Equations

• OmegaCompletePartialOrder.Chain.Option.distrib c = if h : ∃ (n : ℕ), (c n).isSome = true then some (OmegaCompletePartialOrder.Chain.Option.project c h) else none

@[simp]

theorem OmegaCompletePartialOrder.Chain.Option.distrib_none {A : Type u_1} [Preorder A] : distrib none = _root_.Option.none

@[simp]

theorem OmegaCompletePartialOrder.Chain.Option.distrib_some {A : Type u_1} [Preorder A] (i : ℕ) (c : Chain A) : distrib (some i c) = _root_.Option.some c

theorem OmegaCompletePartialOrder.Chain.Option.distrib_cases {A : Type u_1} [Preorder A] {p : Chain (Option A) → Prop} (none : p none) (some : ∀ (i : ℕ) (c : Chain A), p (some i c)) (c : Chain (Option A)) : p c