take_isPrefix_take — Mathlib

English

For any list l and natural numbers m, n, the take m l is a prefix of take n l exactly when m ≤ n or the length of l is ≤ n.

Русский

Для любого списка l и натуральных чисел m, n отношение take m l префикс take n l эквивалентно m ≤ n или длине l ≤ n.

LaTeX

$$$$ l take m <+: l take n \iff m \le n \lor l.length \le n. $$$$

Lean4

@[simp]
theorem take_isPrefix_take {m n : ℕ} : l.take m <+: l.take n ↔ m ≤ n ∨ l.length ≤ n := by
  simp [prefix_take_iff, take_prefix]; omega

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