leftpad_suffix

Mathlib.Data.String.Lemmas

URI: https://scilib.ai/kg/mathlib#String.leftpad_suffix

English

For every n and c, and string s, s is a suffix of leftpad(n,c,s).

Русский

Для каждого n, c и строки s, s является суффиксом leftpad(n,c,s).

LaTeX

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

Lean4

theorem leftpad_suffix (n : ℕ) (c : Char) : ∀ s, IsSuffix s (leftpad n c s)
  | ⟨l⟩ => by simp only [IsSuffix, leftpad, List.leftpad_suffix]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru