toColex_update_lt_self_iff — Mathlib

English

Changing the i-th coordinate to a increases the toColex value precisely when a < x_i.

Русский

Изменение i-й координаты на a увеличивает значение to Colex ровно тогда, когда a < x_i.

LaTeX

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

Lean4

@[simp]
theorem toColex_update_lt_self_iff : toColex (update x i a) < toColex x ↔ a < x i :=
  toLex_update_lt_self_iff (ι := ιᵒᵈ)

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