take_eq_left_iff — Mathlib

English

The equality (x ++ y).take n = x.take n holds iff y = [] or n ≤ x.length.

Русский

Равенство (x ++ y).take n = x.take n выполняется тогда и только тогда, когда y = [] или n ≤ length(x).

LaTeX

$$$ (x ++ y).take n = x.take n \iff y = \emptyset \lor n \le x.length $$$

Lean4

@[simp]
theorem take_eq_left_iff {x y : List α} {n : ℕ} : (x ++ y).take n = x.take n ↔ y = [] ∨ n ≤ x.length := by
  simp [take_append, Nat.sub_eq_zero_iff_le, Or.comm]

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