cutExpand_single_add

Mathlib.Logic.Hydra

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

← MathLib Explorer

English

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

Русский

Если r(a',a), то CutExpand r ({a'} ∪ s) ({a} ∪ s) для любого мультимножества s.

LaTeX

$$$\\mathrm{CutExpand}(r)({a'} + s)({a} + s)$ при $r(a',a)$$$

Lean4

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

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

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

Разделы

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

Аффилиация

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