card_boundaries_eq_succ_length

Mathlib.Combinatorics.Enumerative.Composition

URI: https://scilib.ai/kg/mathlib#Composition.card_boundaries_eq_succ_length

English

The number of boundaries equals length + 1.

Русский

Число границ равно длине плюс единица.

LaTeX

$$$|c.boundaries| = c.length + 1$$$

Lean4

theorem card_boundaries_eq_succ_length : c.boundaries.card = c.length + 1 := by simp [boundaries]

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

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

Разделы

Аффилиация

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