le_update_self_iff — Mathlib

English

The order from the left to an updated element matches the order of the updated coordinate: x ≤ update x i a iff x_i ≤ a.

Русский

Порядок слева к обновленному элементу соответствует порядку обновленной координаты: x ≤ update x i a если и только если x_i ≤ a.

LaTeX

$$$x \le \text{update } x i a \iff x_i \le a$$$

Lean4

@[simp]
theorem le_update_self_iff : x ≤ update x i a ↔ x i ≤ a := by simp [le_update_iff]

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