Theorems · Definition · logic and foundations

Directed.sequence

{α : Type u_1} →
  {β : Type u_2} → [Encodable α] → [Inhabited α] → {r : β → β → Prop} → (f : α → β) → Directed r f → ℕ → α

Given a Directed r function f : α → β defined on an encodable inhabited type, construct a noncomputable sequence such that r (f (x n)) (f (x (n + 1))) and r (f a) (f (x (encode a + 1)).

Defined in

Mathlib.Logic.Encodable.Basic

Cited by

10 results in Mathlib

Foundations

Depth 9 from the axioms · uses Classical.choice

Assumes

EncodableInhabited