cutExpand_zero

Mathlib.Logic.Hydra

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

English

There exists a CutExpand from the empty multiset to a singleton: CutExpand r 0 {x}.

Русский

Существует CutExpand от пустого мультисета к одиночному: CutExpand r 0 {x}.

LaTeX

$$$\\mathrm{CutExpand}(r)(0,\\{x\\})$$$

Lean4

theorem cutExpand_zero {x} : CutExpand r 0 { x } :=
  ⟨0, x, nofun, add_comm 0 _⟩

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

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

Разделы

Аффилиация

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