Theorems · Theorem · combinatorics

Composition.index_exists

∀ {n : ℕ} (c : Composition n) {j : ℕ}, j < n → ∃ i, j < c.sizeUpTo (i + 1) ∧ i < c.length

index_exists asserts there is some i with j < c.sizeUpTo (i+1). In the next definition index we use Nat.find to produce the minimal such index.

Defined in

Mathlib.Combinatorics.Enumerative.Composition

Cited by

2 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext