noncomputable def OrderHom.k_induction.Ξ {α : Type u_1} [CompleteLattice α] (f : α) (Δ : α →o α) : α →o α

Equations

• OrderHom.k_induction.Ξ f Δ = { toFun := fun (x : α) => Δ x ⊓ f, monotone' := ⋯ }

def OrderHom.k_induction.Ξ_iter_antitone {α : Type u_1} [CompleteLattice α] (f : α) (Δ : α →o α) : Antitone fun (x : ℕ) => (⇑(Ξ f Δ))^[x] f

Equations

• ⋯ = ⋯

theorem OrderHom.k_induction.park {α : Type u_1} [CompleteLattice α] (Δ : α →o α) (f : α) (k : ℕ) : Δ ((⇑(Ξ f Δ))^[k] f) ≤ f ↔ Δ ((⇑(Ξ f Δ))^[k] f) ≤ (⇑(Ξ f Δ))^[k] f

theorem OrderHom.lfp_le_of_iter {α : Type u_1} [CompleteLattice α] {Δ : α →o α} {f : α} (k : ℕ) (h : Δ ((fun (x : α) => Δ x ⊓ f)^[k] f) ≤ f) : lfp Δ ≤ f

k-induction

noncomputable def OrderHom.k_coinduction.Ξ {α : Type u_1} [CompleteLattice α] (f : α) (Δ : α →o α) : α →o α

Equations

• OrderHom.k_coinduction.Ξ f Δ = { toFun := fun (x : α) => Δ x ⊔ f, monotone' := ⋯ }

def OrderHom.k_coinduction.Ξ_iter_monotone {α : Type u_1} [CompleteLattice α] (f : α) (Δ : α →o α) : Monotone fun (x : ℕ) => (⇑(Ξ f Δ))^[x] f

Equations

• ⋯ = ⋯

theorem OrderHom.k_coinduction.park {α : Type u_1} [CompleteLattice α] (Δ : α →o α) (f : α) (k : ℕ) : f ≤ Δ ((⇑(Ξ f Δ))^[k] f) ↔ (⇑(Ξ f Δ))^[k] f ≤ Δ ((⇑(Ξ f Δ))^[k] f)

theorem OrderHom.le_gfp_of_iter {α : Type u_1} [CompleteLattice α] {Δ : α →o α} {f : α} (k : ℕ) (h : f ≤ Δ ((fun (x : α) => Δ x ⊔ f)^[k] f)) : f ≤ gfp Δ

k-coinduction