Equations
- IsInfiniteDescendingChain r c = ∀ (i : ℕ), r (c (i + 1)) (c i)
Instances For
Equations
- descendingChain r z 0 = z
- descendingChain r z i.succ = Classical.epsilon fun (y : α) => r y (descendingChain r z i) ∧ ¬Acc r y
Instances For
@[simp]
theorem
isInfiniteDescendingChain_of_non_acc
{α : Sort u}
(r : α → α → Prop)
(z : α)
(hz : ¬Acc r z)
: