rel_or_eq_of_le — Mathlib

English

A variant of the previous fact: if i < j then x_i ~ x_j holds.

Русский

Вариант предыдущего факта: если i < j, то x_i относится к x_j.

LaTeX

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

Lean4

theorem rel_or_eq_of_le [r.IsTrans] (x : RelSeries r) {i j : Fin (x.length + 1)} (h : i ≤ j) :
    x i ~[r] x j ∨ x i = x j :=
  (Fin.lt_or_eq_of_le h).imp (x.rel_of_lt ·) (by rw [·])

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