Theorems · Theorem · logic and foundations

Relation.cutExpand_closed

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

CutExpand preserves leftward-closedness under a relation.

Defined in

Mathlib.Logic.Hydra

Cited by

0 results in Mathlib

Foundations

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

Assumes

Std.Irrefl