Mathlib v3 is deprecated. Go to Mathlib v4

Theorem finset.coe_ssubset

Modification history

2020-11-08 16:26

src/data/finset/basic.lean

chore(data/finset/basic): use `has_coe_t` for coercion of `finset` to `set` (#4917)

Modified finset.coe_ssubset View on Github →

2020-06-18 11:39

src/data/finset.lean

chore(data/finset): minor review (#3105)

Modified finset.coe_ssubset View on Github →

2018-08-10 09:04

data/finset.lean

feat(data/set/finite): card_image_of_injective and other minor lemmas (#245)

Added finset.coe_ssubset View on Github →