leftpad_prefix — Mathlib

English

The left-padding prefix is a prefix of leftpad(n,c,s): replicate(n - length(s)) c is a prefix of leftpad(n,c,s).

Русский

Префикс левого заполнения является префиксом leftpad(n,c,s): replicate(n - length(s)) c — это префикс leftpad(n,c,s).

LaTeX

$$$ \text{IsPrefix}(\text{replicate}(n - \operatorname{length}(s))\, c,\ \text{leftpad}(n,c,s)). $$$

Lean4

theorem leftpad_prefix (n : ℕ) (c : Char) : ∀ s, IsPrefix (replicate (n - length s) c) (leftpad n c s)
  | ⟨l⟩ => by simp only [IsPrefix, replicate, leftpad, String.length, List.leftpad_prefix]

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