le_toLex_update_self_iff — Mathlib

English

The relation x ≤ a in the Lex order corresponds to the coordinate-wise inequality x_i ≤ a in the i-th slot.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem le_toLex_update_self_iff : toLex x ≤ toLex (update x i a) ↔ x i ≤ a := by
  simp_rw [le_iff_lt_or_eq, lt_toLex_update_self_iff, toLex_inj, eq_update_self_iff]

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