update_le_iff — Mathlib

English

For x,y, i,a, the condition update x i a ≤ y is equivalent to a ≤ y_i and, for all j ≠ i, x_j ≤ y_j.

Русский

Обновление x на позиции i до a меньше или равно y тогда и только тогда a ≤ y_i и для всех j ≠ i выполняется x_j ≤ y_j.

LaTeX

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

Lean4

theorem update_le_iff : Function.update x i a ≤ y ↔ a ≤ y i ∧ ∀ (j) (_ : j ≠ i), x j ≤ y j :=
  Function.forall_update_iff _ fun j z ↦ z ≤ y j

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