Finset

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

Statistics

Metric	Count
Definitions	0
Theorems cons_mem_piFinset_cons, insertNth_mem_piFinset_insertNth, mem_piFinset_iff_last_init, mem_piFinset_iff_pivot_removeNth, mem_piFinset_iff_zero_tail, snoc_mem_piFinset_snoc, card_consEquiv_filter_piFinset, card_insertNthEquiv_filter_piFinset, card_snocEquiv_filter_piFinset, filter_piFinset_eq_map_consEquiv, filter_piFinset_eq_map_insertNthEquiv, filter_piFinset_eq_map_snocEquiv, map_consEquiv_filter_piFinset, map_insertNthEquiv_filter_piFinset, map_snocEquiv_filter_piFinset	15
Total	15

Fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cons_mem_piFinset_cons 📖	mathematical	—	Finset Finset.instMembership Fintype.piFinset fintype cons	—	cons_zero tail_cons
insertNth_mem_piFinset_insertNth 📖	mathematical	—	Finset Finset.instMembership Fintype.piFinset fintype insertNth succAbove	—	mem_piFinset_iff_pivot_removeNth insertNth_apply_same removeNth_insertNth
mem_piFinset_iff_last_init 📖	mathematical	—	Finset Finset.instMembership Fintype.piFinset fintype init	—	—
mem_piFinset_iff_pivot_removeNth 📖	mathematical	—	Finset Finset.instMembership Fintype.piFinset fintype succAbove removeNth	—	forall_iff_succAbove
mem_piFinset_iff_zero_tail 📖	mathematical	—	Finset Finset.instMembership Fintype.piFinset fintype tail	—	—
snoc_mem_piFinset_snoc 📖	mathematical	—	Finset Finset.instMembership Fintype.piFinset fintype snoc	—	init_snoc snoc_last

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_consEquiv_filter_piFinset 📖	mathematical	—	card filter Fin.tail Fintype.piFinset Fin.fintype Finset	—	card_product map_consEquiv_filter_piFinset card_map
card_insertNthEquiv_filter_piFinset 📖	mathematical	—	card filter Fin.removeNth Fintype.piFinset Fin.fintype Fin.succAbove Finset	—	card_product map_insertNthEquiv_filter_piFinset card_map
card_snocEquiv_filter_piFinset 📖	mathematical	—	card filter Fin.init Fintype.piFinset Fin.fintype Finset	—	card_product map_snocEquiv_filter_piFinset card_map
filter_piFinset_eq_map_consEquiv 📖	mathematical	—	filter Fin.tail Fintype.piFinset Fin.fintype map Equiv.toEmbedding Fin.consEquiv SProd.sprod Finset instSProd	—	map_map Function.Embedding.equiv_symm_toEmbedding_trans_toEmbedding map_refl
filter_piFinset_eq_map_insertNthEquiv 📖	mathematical	—	filter Fin.removeNth Fintype.piFinset Fin.fintype map Equiv.toEmbedding Fin.insertNthEquiv SProd.sprod Finset instSProd Fin.succAbove	—	map_map Function.Embedding.equiv_symm_toEmbedding_trans_toEmbedding map_refl
filter_piFinset_eq_map_snocEquiv 📖	mathematical	—	filter Fin.init Fintype.piFinset Fin.fintype map Equiv.toEmbedding Fin.snocEquiv SProd.sprod Finset instSProd	—	map_map Function.Embedding.equiv_symm_toEmbedding_trans_toEmbedding map_refl
map_consEquiv_filter_piFinset 📖	mathematical	—	map Equiv.toEmbedding Equiv.symm Fin.consEquiv filter Fin.tail Fintype.piFinset Fin.fintype SProd.sprod Finset instSProd	—	ext Fin.cons_zero Fin.cons_succ
map_insertNthEquiv_filter_piFinset 📖	mathematical	—	map Equiv.toEmbedding Equiv.symm Fin.insertNthEquiv filter Fin.removeNth Fintype.piFinset Fin.fintype SProd.sprod Finset instSProd Fin.succAbove	—	ext Fin.forall_iff_succAbove Fin.insertNth_apply_same Fin.insertNth_apply_succAbove
map_snocEquiv_filter_piFinset 📖	mathematical	—	map Equiv.toEmbedding Equiv.symm Fin.snocEquiv filter Fin.init Fintype.piFinset Fin.fintype SProd.sprod Finset instSProd	—	ext Fin.snoc_last Fin.snoc_castSucc

---

← Back to Index