Theorems · Theorem · logic and foundations

Relation.acc_of_singleton

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

A multiset is accessible under CutExpand if all its singleton subsets are, assuming r is irreflexive.

Defined in

Mathlib.Logic.Hydra

Cited by

2 results in Mathlib

Foundations

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

Assumes

Std.Irrefl