cutExpand_add_single

Mathlib.Logic.Hydra

URI: https://scilib.ai/kg/mathlib#Relation.cutExpand_add_single

← MathLib Explorer

English

If r(a',a) then CutExpand r (s + {a'}) (s + {a}).

Русский

Если r(a',a), то CutExpand r (s ∪ {a'}) (s ∪ {a}).

LaTeX

$$$\\mathrm{CutExpand}(r)(s + \\{a'\\}, s + \\{a\\})$ given $r(a',a)$$$

Lean4

theorem cutExpand_add_single {a' a : α} (s : Multiset α) (h : r a' a) : CutExpand r (s + { a' }) (s + { a }) :=
  (cutExpand_add_left s).2 <| cutExpand_singleton_singleton h

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru