take_eq_take — Mathlib

English

Two takes are equal if and only if the two lengths agree after applying min with the actual list length.

Русский

Два взятия равны тогда и только тогда, когда получаются равные минимальные значения длины и запрошенных длин.

LaTeX

$$$ \\forall {x,m,n},\\; \\mathrm{take}(m,x) = \\mathrm{take}(n,x) \\iff \\min(m, |x|) = \\min(n, |x|) $$$

Lean4

@[simp]
theorem take_eq_take {x : T} {m n : ℕ} : take m x = take n x ↔ m ⊓ x.val.length = n ⊓ x.val.length := by
  simp [Subtype.ext_iff]
    -- ### `subAt`

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