lt_update_self_iff

Mathlib.Order.Basic

URI: https://scilib.ai/kg/mathlib#lt_update_self_iff

English

Updating at i preserves the order relation strictly: x < update x i a iff x_i < a.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem lt_update_self_iff : x < update x i a ↔ x i < a := by simp [lt_iff_le_not_ge]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru