toColex_update_le_self_iff — Mathlib

English

The le_toLex relation for Pi-types equates the Lex and the PartialOrder le: the le relation on toLex x and toLex(update x i a) corresponds to a's le relation.

Русский

Отношение ≤ для toLex в Pi-представлении совпадает с ℓ-отношением на координате обновления.

LaTeX

$$$\\mathrm{toLex}(x) \\le \\mathrm{toLex}(\\mathrm{update}(x,i,a)) \\iff (a \\le x_i).$$$

Lean4

@[simp]
theorem toColex_update_le_self_iff : toColex (update x i a) ≤ toColex x ↔ a ≤ x i :=
  toLex_update_le_self_iff (ι := ιᵒᵈ)

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