English
For Pi-type functions, the comparison of toLex under an update matches the comparison of the updated coordinate with the old one, expressed as an equivalence of inequalities.
Русский
Для Pi-типов сравнение toLex после обновления координаты совпадает с сравнением новой координаты с исходной.
LaTeX
$$$\\forall x,i,a:\\, \\mathrm{toLex}(\,x\,) \\leqslant \\mathrm{toLex}(\\mathrm{update}(x,i,a)) \\iff (\\text{сложное условие об упорядоченности}).$$$
Lean4
@[simp]
theorem toLex_update_lt_self_iff : toLex (update x i a) < toLex x ↔ a < x i :=
by
refine ⟨?_, fun h => toLex_strictMono <| update_lt_self_iff.2 h⟩
rintro ⟨j, hj, h⟩
dsimp at h
obtain rfl : j = i := by
by_contra H
rw [update_of_ne H] at h
exact h.false
rwa [update_self] at h
