rel_of_lt

Mathlib.Order.RelSeries

URI: https://scilib.ai/kg/mathlib#RelSeries.rel_of_lt

← MathLib Explorer

English

If r is transitive and x is a RelSeries r, then for i < j, x_i is related to x_j by r.

Русский

Если r транзитивно и x — RelSeries r, то для i<j x_i r x_j.

LaTeX

$$$ [r.IsTrans]\\; (x:RelSeries\\; r)\\ {i j:\\mathrm{Fin}(x.length+1)}\\ (i

Lean4

theorem rel_of_lt [r.IsTrans] (x : RelSeries r) {i j : Fin (x.length + 1)} (h : i < j) : x i ~[r] x j :=
  (Fin.liftFun_iff_succ (· ~[r] ·)).mpr x.step h

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

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

Разделы

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

Аффилиация

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