le_insertNth_iff — Mathlib

English

Again a coordinate-wise characterization, but for the reverse inequality.

Русский

Определение обратной связи для неравенства: q ≤ i.insertNth x p эквивалентно q i ≤ x и tail ≤ p.

LaTeX

$$$$ q \le i.insertNth x p \iff q i \le x \wedge (\lambda j. q (i.succAbove j)) \le p $$$$

Lean4

theorem le_insertNth_iff {i : Fin (n + 1)} {x : α i} {p : ∀ j, α (i.succAbove j)} {q : ∀ j, α j} :
    q ≤ i.insertNth x p ↔ q i ≤ x ∧ (fun j ↦ q (i.succAbove j)) ≤ p := by simp [Pi.le_def, forall_iff_succAbove i]

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