lt_toColex_update_self_iff

Mathlib.Order.PiLex

URI: https://scilib.ai/kg/mathlib#Pi.lt_toColex_update_self_iff

English

For x, i, a, the relation toColex x < toColex(update x i a) is equivalent to a < x_i.

Русский

Для x, i, a выражение toColex x < toColex(update x i a) эквивалентно a < x_i.

LaTeX

$$$\\mathrm{toColex}(x) < \\mathrm{toColex}(\\mathrm{update}(x,i,a)) \\iff a < x_i.$$$

Lean4

@[simp]
theorem lt_toColex_update_self_iff : toColex x < toColex (update x i a) ↔ x i < a :=
  lt_toLex_update_self_iff (ι := ιᵒᵈ)

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

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

Разделы

Аффилиация

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