Theorems · Theorem · logic and foundations

Relation.cutExpand_iff

∀ {α : Type u_1} {r : α → α → Prop} [inst : DecidableEq α] [Std.Irrefl r] {s' s : Multiset α},
  Relation.CutExpand r s' s ↔ ∃ t a, (∀ a' ∈ t, r a' a) ∧ a ∈ s ∧ s' = s.erase a + t

Defined in

Mathlib.Logic.Hydra

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqStd.Irrefl