Theorems · Theorem · combinatorics
List.range_bind_sublistsLen_perm
∀ {α : Type u} (l : List α), (List.flatMap (fun n => List.sublistsLen n l) (List.range (l.length + 1))).Perm l.sublists'- Defined in
- Mathlib.Data.List.Sublists
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 37 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- List.sublistsLenstatement and proof · cited by 19
- List.sublists'_consproof · cited by 9
- List.sublistsLen_succ_consproof · cited by 5
- List.sublistsLen_zeroproof · cited by 5
- List.flatMap_append_permproof · cited by 4
- List.sublistsLen_of_length_ltproof · cited by 1
Cited by1
Results whose statement or proof uses this declaration.
- Multiset.bind_powerset_lenproof · cited by 2