Theorems · Theorem · logic and foundations

Acc.cutExpand

∀ {α : Type u_1} {r : α → α → Prop} [Std.Irrefl r] {a : α}, Acc r a → Acc (Relation.CutExpand r) {a}

A singleton {a} is accessible under CutExpand r if a is accessible under r, assuming r is irreflexive.

Defined in

Mathlib.Logic.Hydra

Cited by

1 results in Mathlib

Foundations

Depth 57 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Std.Irrefl