update_le_update_iff — Mathlib

English

The comparison between two updates is equivalent to comparing the updated coordinates and comparing the remaining coordinates coordinatewise.

Русский

Сравнение двух обновлений эквивалентно сравнению обновленных координат и сравнению остальных координат по отдельности.

LaTeX

$$$\text{update } x i a \le \text{update } y i b \iff a \le b \land \forall j (j \neq i), x_j \le y_j$$$

Lean4

theorem update_le_update_iff : Function.update x i a ≤ Function.update y i b ↔ a ≤ b ∧ ∀ (j) (_ : j ≠ i), x j ≤ y j :=
  by simp +contextual [update_le_iff]

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