length_leftpad — Mathlib

English

The length of leftpad(n,c,s) is max(n, s.length).

Русский

Длина leftpad(n,c,s) равна max(n, length(s)).

LaTeX

$$$ \forall n:\mathbb{N},\forall c\in \text{Char},\forall s:\text{String},\ (leftpad(n,c,s)).length = \max(n, s.length). $$$

Lean4

/-- The length of the String returned by `String.leftpad n a c` is equal
  to the larger of `n` and `s.length` -/
@[simp]
theorem length_leftpad (n : ℕ) (c : Char) : ∀ (s : String), (leftpad n c s).length = max n s.length
  | ⟨s⟩ => by simp only [leftpad, String.length, List.length_leftpad]

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