update_lt_update_iff — Mathlib

English

Updating both sides at the same index preserves strict order: update x i a < update x i b iff a < b.

Русский

Обновление обеих сторон одинаково по индексу сохраняет строгий порядок: update x i a < update x i b, тогда как a < b.

LaTeX

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

Lean4

@[simp]
theorem update_lt_update_iff : update x i a < update x i b ↔ a < b :=
  lt_iff_lt_of_le_iff_le' update_le_update_iff' update_le_update_iff'

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