English
CutExpand preserves leftward-closedness under a relation: if p is preserved by r and holds on s, then it holds on s'.
Русский
CutExpand сохраняет левую закрытость под отношением: если p сохраняется по r и выполняется на s, то выполняется на s'.
LaTeX
$$$\\forall p,\\; (\\forall {a' a}, r(a',a) \\Rightarrow p(a) \\Rightarrow p(a)) \\to (\\mathrm{CutExpand}(r)(s',s) \\Rightarrow (\\forall a\\in s, p(a) ) \\Rightarrow \\forall a\\in s', p(a))$$$
Lean4
/-- `CutExpand` preserves leftward-closedness under a relation. -/
theorem cutExpand_closed [IsIrrefl α r] (p : α → Prop) (h : ∀ {a' a}, r a' a → p a → p a') {s' s : Multiset α} :
CutExpand r s' s → (∀ a ∈ s, p a) → ∀ a ∈ s', p a := by
classical
rw [cutExpand_iff]
rintro ⟨t, a, hr, ha, rfl⟩ hsp a' h'
obtain (h' | h') := mem_add.1 h'
exacts [hsp a' (mem_of_mem_erase h'), h (hr a' h') (hsp a ha)]
