trans

Mathlib.Computability.ContextFreeGrammar

URI: https://scilib.ai/kg/mathlib#ContextFreeGrammar.Derives.trans

← MathLib Explorer

English

If u derives v and v derives w, then u derives w.

Русский

Если u выводится в v, а v выводится в w, то u выводится в w.

LaTeX

$$$\forall u\forall v\forall w,\; g.Derives\, u\, v \wedge g.Derives\, v\, w \Rightarrow g.Derives\, u\, w$$$

Lean4

@[trans]
theorem trans {u v w : List (Symbol T g.NT)} (huv : g.Derives u v) (hvw : g.Derives v w) : g.Derives u w :=
  Relation.ReflTransGen.trans huv hvw

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

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

Разделы

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

Аффилиация

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