mathlib3
a60ef7c9 - feat(data/list/sort): subperm sorted implies sublist (#10892)

Commit
4 years ago
feat(data/list/sort): subperm sorted implies sublist (#10892) A "sub" version of the lemma directly above.
Author
Parents
Loading