lt_trans

Mathlib.Algebra.Order.CauSeq.Basic

URI: https://scilib.ai/kg/mathlib#CauSeq.lt_trans

English

Let f, g, h be CauSeq(α, abs). If f < g and g < h, then f < h.

Русский

Пусть f, g, h — CauSeq(α, abs). если f < g и g < h, то f < h.

LaTeX

$$$\forall f,g,h \in \mathrm{CauSeq}(\alpha,\mathrm{abs}),\; f

Lean4

theorem lt_trans {f g h : CauSeq α abs} (fg : f < g) (gh : g < h) : f < h :=
  show Pos (h - f) by
    convert add_pos fg gh using 1
    simp

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

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

Разделы

Аффилиация

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