update_le_update_iff' — Mathlib

English

Same as update_le_update_iff but with a simplified statement using a single equivalence between the two comparisons.

Русский

То же самое, что и update_le_update_iff', но выражено более компактно через эквивалентность двух сравнений.

LaTeX

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

Lean4

@[simp]
theorem update_le_update_iff' : update x i a ≤ update x i b ↔ a ≤ b := by simp [update_le_update_iff]

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