Mathlib v3 is deprecated. Go to Mathlib v4

Theorem subset_of_subset_of_eq

Modification history

2023-01-08 09:48

src/order/rel_classes.lean

feat(data/{set,finset}/basic): Convenience lemmas (#17957) …

Added subset_of_subset_of_eq View on Github →