perm_insertIdx_iff_of_le — Mathlib

English

If m ≤ |l1| and n ≤ |l2|, then (l1.insertIdx m a) ~ (l2.insertIdx n a) iff l1 ~ l2.

Русский

Если m ≤ |l1| и n ≤ |l2|, тогда (l1.insertIdx m a) ~ (l2.insertIdx n a) эквивалентно l1 ~ l2.

LaTeX

$$$\\forall {l_1 l_2} {m n} (hm : m \\le |l_1|) (hn : n \\le |l_2|) (a), (l_1.insertIdx m a) \\sim (l_2.insertIdx n a) \\iff l_1 \\sim l_2.$$$

Lean4

theorem perm_insertIdx_iff_of_le {l₁ l₂ : List α} {m n : ℕ} (hm : m ≤ l₁.length) (hn : n ≤ l₂.length) (a : α) :
    l₁.insertIdx m a ~ l₂.insertIdx n a ↔ l₁ ~ l₂ := by
  rw [rel_congr_left (perm_insertIdx _ _ hm), rel_congr_right (perm_insertIdx _ _ hn), perm_cons]

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