drop — Mathlib

English

If l1 is a prefix of l2, then dropping n elements preserves prefix relation after adjusting with prefix equivalence.

Русский

Если l1 префикс l2, то удаление n элементов сохраняет отношение префикса после соответствующего преобразования.

LaTeX

$$$$ h : l1 <+: l2 \Rightarrow l1.drop n <+: l2.drop n. $$$$

Lean4

@[gcongr]
theorem drop (h : l₁ <+: l₂) (n : ℕ) : l₁.drop n <+: l₂.drop n := by rw [prefix_iff_eq_take.mp h, drop_take];
  apply take_prefix

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