le_toColex_update_self_iff — Mathlib

English

The Leonine form preserves ≤ under updates for Colex: x ≤ toColex(update x i a) iff x_i ≤ a.

Русский

Сохранение нестрогое ≤ сохраняется при обновлении координаты в Colex: x ≤ toColex(update x i a) эквивалентно x_i ≤ a.

LaTeX

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

Lean4

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

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