cutExpand_pair_left

Mathlib.Logic.Hydra

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

← MathLib Explorer

English

If hr: r a' a, then CutExpand r {a', b} {a, b}.

Русский

Если hr: r(a',a), то CutExpand r {a', b} {a, b}.

LaTeX

$$$\\forall a',a,b:\\; hr:\\; r(a',a) \\Rightarrow \\mathrm{CutExpand}(r)({a',b},{a,b})$$$

Lean4

theorem cutExpand_pair_left {a' a b} (hr : r a' a) : CutExpand r { a', b } { a, b } :=
  (cutExpand_add_right { b }).2 (cutExpand_singleton_singleton hr)

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

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

Разделы

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

Аффилиация

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