Fin

📁 Source: Mathlib/Data/Finset/Fin.lean

Statistics

Metric	Count
Definitions attachFin	1
Theorems attachFin_ssubset_attachFin, attachFin_ssubset_attachFin_iff, attachFin_subset_attachFin, attachFin_subset_attachFin_iff, card_attachFin, coe_attachFin, image_val_attachFin, map_valEmbedding_attachFin, mem_attachFin	9
Total	10

Finset

Definitions

Name	Category	Theorems
attachFin 📖	CompOp	18 math math: Fin.attachFin_Iic, Fin.attachFin_Ioo_eq_Ioi, coe_attachFin, attachFin_ssubset_attachFin, Fin.attachFin_Icc, Fin.attachFin_Ico_eq_Ici, card_attachFin, Fin.attachFin_uIcc, Fin.attachFin_Ico, Fin.attachFin_Ioo, image_val_attachFin, Fin.attachFin_Iio, attachFin_ssubset_attachFin_iff, map_valEmbedding_attachFin, attachFin_subset_attachFin, attachFin_subset_attachFin_iff, mem_attachFin, Fin.attachFin_Ioc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
attachFin_ssubset_attachFin 📖	mathematical	Finset instHasSSubset	attachFin HasSSubset.SSubset.subset instHasSubset instIsNonstrictStrictOrderSubsetSSubset	—	HasSSubset.SSubset.subset instIsNonstrictStrictOrderSubsetSSubset
attachFin_ssubset_attachFin_iff 📖	mathematical	—	Finset instHasSSubset attachFin	—	map_ssubset_map map_valEmbedding_attachFin
attachFin_subset_attachFin 📖	mathematical	Finset instHasSubset	attachFin	—	—
attachFin_subset_attachFin_iff 📖	mathematical	—	Finset instHasSubset attachFin	—	map_subset_map map_valEmbedding_attachFin
card_attachFin 📖	mathematical	—	card attachFin	—	Multiset.card_pmap
coe_attachFin 📖	mathematical	—	SetLike.coe Finset instSetLike attachFin Set.preimage	—	Set.ext
image_val_attachFin 📖	mathematical	—	image attachFin	—	coe_injective coe_image coe_attachFin Set.image_preimage_eq_iff
map_valEmbedding_attachFin 📖	mathematical	—	map Fin.valEmbedding attachFin	—	map_eq_image image_val_attachFin
mem_attachFin 📖	mathematical	—	Finset instMembership attachFin	—	Multiset.mem_pmap

---

← Back to Index