update_le_self_iff

Mathlib.Order.Basic

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

English

The comparison of an updated element with the original one depends only on the updated coordinate.

Русский

Сравнение обновленного элемента с исходным зависит только от обновленной координаты.

LaTeX

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

Lean4

@[simp]
theorem update_le_self_iff : update x i a ≤ x ↔ a ≤ x i := by simp [update_le_iff]

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

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

Разделы

Аффилиация

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