theorem OmegaCompletePartialOrder.iterate_le_succ {α : Type u_1} [OmegaCompletePartialOrder α] (f : α →𝒄 α) (x : α) (hx : x ≤ f x) (n : ℕ) : (⇑f)^[n] x ≤ (⇑f)^[n + 1] x

def OmegaCompletePartialOrder.Chain.iterate {α : Type u_1} [OmegaCompletePartialOrder α] (f : α →𝒄 α) (x : α) (hx : x ≤ f x) : Chain α

the sequence of iterates of a function

Equations

• OmegaCompletePartialOrder.Chain.iterate f x hx = { toFun := fun (n : ℕ) => (⇑f)^[n] x, monotone' := ⋯ }

@[simp]

theorem OmegaCompletePartialOrder.Chain.iterate_apply {α : Type u_1} [OmegaCompletePartialOrder α] (f : α →𝒄 α) (x : α) (hx : x ≤ f x) (n : ℕ) : (iterate f x hx) n = (⇑f)^[n] x

def OmegaCompletePartialOrder.fix {α : Type u_1} [OmegaCompletePartialOrder α] [OrderBot α] (f : α →𝒄 α) : α

the fixed point of a continuous function

Equations

• OmegaCompletePartialOrder.fix f = OmegaCompletePartialOrder.ωSup (OmegaCompletePartialOrder.Chain.iterate f ⊥ ⋯)

theorem OmegaCompletePartialOrder.fix_eq {α : Type u_1} [OmegaCompletePartialOrder α] [OrderBot α] (f : α →𝒄 α) : fix f = f (fix f)