coe_ofLE — Mathlib

English

Given a RelSeries x and a relation refinement h : r ≤ s, one can lift x to a RelSeries s with the same length and with step transformed by h.

Русский

Имея RelSeries x и отображение перехода h: r ≤ s, можно поднять x до RelSeries s той же длины и со сдвигом, перестроенным по h.

LaTeX

$$$ ofLE:\\; x:\\text{RelSeries } r \\to {s:\\text{SetRel } α α} \\; (h: r \\le s) \\Rightarrow \\text{RelSeries } s. $$$

Lean4

theorem coe_ofLE (x : RelSeries r) {s : SetRel α α} (h : r ≤ s) : (x.ofLE h : _ → _) = x :=
  rfl

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