def IsInfiniteDescendingChain {α : Sort u} (r : α → α → Prop) (c : ℕ → α) : Prop

Equations

• IsInfiniteDescendingChain r c = ∀ (i : ℕ), r (c (i + 1)) (c i)

noncomputable def descendingChain {α : Sort u} (r : α → α → Prop) (z : α) : ℕ → α

Equations

• descendingChain r z 0 = z
• descendingChain r z i.succ = Classical.epsilon fun (y : α) => r y (descendingChain r z i) ∧ ¬Acc r y

theorem not_acc_iff {α : Sort u} (r : α → α → Prop) {x : α} : ¬Acc r x ↔ ∃ (y : α), r y x ∧ ¬Acc r y

@[simp]

theorem descending_chain_zero {α : Sort u} (r : α → α → Prop) (z : α) : descendingChain r z 0 = z

theorem isInfiniteDescendingChain_of_non_acc {α : Sort u} (r : α → α → Prop) (z : α) (hz : ¬Acc r z) : IsInfiniteDescendingChain r (descendingChain r z)