eq_ones_iff_le_length

Mathlib.Combinatorics.Enumerative.Composition

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

English

c = ones n iff n ≤ c.length.

Русский

c = ones n тогда и только тогда, когда n ≤ c.length.

LaTeX

$$$ c = \\text{ones}(n) \\iff n \\le c.length $$$

Lean4

theorem eq_ones_iff_le_length {c : Composition n} : c = ones n ↔ n ≤ c.length := by
  simp [eq_ones_iff_length, le_antisymm_iff, c.length_le]

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

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

Разделы

Аффилиация

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