lt_toLex_update_self_iff — Mathlib

English

For x : ∀ i, β_i, i ∈ ι and a ∈ β_i, we have toLex x < toLex(update x i a) if and only if x_i < a.

Русский

Для x: ∀ i, β_i и i ∈ ι, a ∈ β_i верно: toLex x < toLex(update x i a) тогда и только если x_i < a.

LaTeX

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

Lean4

@[simp]
theorem lt_toLex_update_self_iff : toLex x < toLex (update x i a) ↔ x i < a :=
  by
  refine ⟨?_, fun h => toLex_strictMono <| lt_update_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

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