take_take — Mathlib

English

Taking prefixes twice is the same as taking the minimum of the two lengths: take m (take n x) = take (min(m,n)) x.

Русский

Два взятия префиксов эквивалентны взятию префикса длины min(m,n): take m (take n x) = take (min(m,n)) x.

LaTeX

$$$ \\text{take\_take} : \\forall m,n,\\; \\mathrm{take}(m, \\mathrm{take}(n, x)) = \\mathrm{take}(\\min(m,n), x) $$$

Lean4

@[simp]
theorem take_take (m n : ℕ) (x : T) : take m (take n x) = take (m ⊓ n) x := by simp [Subtype.ext_iff, List.take_take]

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