Theorem List.subperm_of_sublists'_subperm_sublists'

Modification history

2026-03-10 20:04
Mathlib/Data/List/Sublists.lean
feat(Data/Multiset/Powerset): show injectivity and monotonicity of powerset (#35465) …
Added List.subperm_of_sublists'_subperm_sublists'View on Github →