ofLE — Mathlib

English

For x a RelSeries with a transitive relation r, if i ≤ j then either x_i ~ x_j or x_i = x_j.

Русский

Для x — RelSeries с отношением r, если i ≤ j, то либо x_i ~ x_j, либо x_i = x_j.

LaTeX

$$$ [r.IsTrans] (x:RelSeries\\; r)\\; (i \\le j) \\Rightarrow (x_i ~[r] x_j) \\lor (x_i = x_j). $$$

Lean4

/-- Given two relations `r, s` on `α` such that `r ≤ s`, any relation series of `r` induces a relation
series of `s`
-/
@[simps!]
def ofLE (x : RelSeries r) {s : SetRel α α} (h : r ≤ s) : RelSeries s
    where
  length := x.length
  toFun := x
  step _ := h <| x.step _

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