rightInvSeq_drop — Mathlib

English

Taking the first j letters of the left-inverse sequence equals the leftInvSeq of the first j letters of ω.

Русский

Взятие первых j букв левой обратной последовательности равняется leftInvSeq для первых j букв ω.

LaTeX

$$$\\mathrm{lis}(\\omega.\\mathrm{take}\\, j) = (\\mathrm{lis}\\, \\omega).\\mathrm{take}\\, j$$$

Lean4

theorem rightInvSeq_drop (ω : List B) (j : ℕ) : ris(ω.drop j) = (ris ω).drop j := by
  induction j generalizing ω with
  | zero => simp
  | succ j ih₁ =>
    induction ω with
    | nil => simp
    | cons k ω _ => rw [drop_succ_cons, ih₁ ω, rightInvSeq, drop_succ_cons]

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