cutExpand_singleton_singleton

Mathlib.Logic.Hydra

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

English

If r(x',x) holds, then CutExpand r {x'} {x}.

Русский

Если выполнено r(x',x), то CutExpand r {x'} {x}.

LaTeX

$$$\\mathrm{CutExpand}(r)(\\{x'\\},\\{x\\})$ whenever $r(x',x)$$$

Lean4

theorem cutExpand_singleton_singleton {x' x} (h : r x' x) : CutExpand r { x' } { x } :=
  cutExpand_singleton fun a h ↦ by rwa [mem_singleton.1 h]

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

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

Разделы

Аффилиация

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