le_update_iff — Mathlib

English

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

Русский

Для функций x,y и индексов i и значений a: x ≤ обновление y в позиции i на a эквивалентно x_i ≤ a и для всех j ≠ i выполняется x_j ≤ y_j.

LaTeX

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

Lean4

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

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