insertNth_le_iff — Mathlib

English

Characterizes when the inserted sequence is below another tuple in the coordinate-wise order.

Русский

Характеризуется, когда вставленный кортеж находится снизу другого кортежа по покоординатной возрастанию.

LaTeX

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

Lean4

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

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