toLex_update_le_self_iff — Mathlib

English

The Lex-ordered relation lifts to the Colex ordering: x ≤ a in toColex corresponds to x_i ≤ a in the i-th coordinate.

Русский

Отношение x ≤ a в порядке toColex соответствует x_i ≤ a в i-й координате.

LaTeX

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

Lean4

@[simp]
theorem toLex_update_le_self_iff : toLex (update x i a) ≤ toLex x ↔ a ≤ x i := by
  simp_rw [le_iff_lt_or_eq, toLex_update_lt_self_iff, toLex_inj, update_eq_self_iff]

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