Fin

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

Statistics

Metric	Count
Definitions	0
Theorems Iio_castSucc, Iio_last_eq_map, Ioi_succ, Ioi_zero_eq_map, card_filter_univ_eq_vector_get_eq_count, card_filter_univ_succ, card_filter_univ_succ', card_filter_val_lt, lt_card_filter_univ_iff_apply_of_imp, map_valEmbedding_univ, image_fin_univ, sup_fin_univ	12
Total	12

Fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Iio_castSucc 📖	mathematical	—	Finset.Iio PartialOrder.toPreorder instPartialOrder instLocallyFiniteOrderBot Finset.map castSuccEmb	—	map_castSuccEmb_Iio
Iio_last_eq_map 📖	mathematical	—	Finset.Iio PartialOrder.toPreorder instPartialOrder instLocallyFiniteOrderBot Finset.map castSuccEmb Finset.univ fintype	—	Finset.coe_injective Set.ext Finset.coe_Iio Finset.coe_map Set.image_congr Finset.coe_univ Set.image_univ range_castSucc
Ioi_succ 📖	mathematical	—	Finset.Ioi PartialOrder.toPreorder instPartialOrder instLocallyFiniteOrderTop Finset.map succEmb	—	map_succEmb_Ioi
Ioi_zero_eq_map 📖	mathematical	—	Finset.Ioi PartialOrder.toPreorder instPartialOrder instLocallyFiniteOrderTop Finset.map succEmb Finset.univ fintype	—	Finset.coe_injective Set.ext Finset.coe_Ioi Finset.coe_map Set.image_congr Finset.coe_univ Set.image_univ range_succ
card_filter_univ_eq_vector_get_eq_count 📖	mathematical	—	Finset.card Finset.filter List.Vector.get Finset.univ fintype List.Vector.toList	—	Finset.filter.congr_simp Finset.univ_eq_empty isEmpty' Finset.filter_empty List.Vector.toList_empty card_filter_univ_succ' List.Vector.get_cons_zero List.Vector.toList_cons List.Vector.get_cons_succ add_comm
card_filter_univ_succ 📖	mathematical	—	Finset.card Finset.filter Finset.univ fintype	—	succ_injective univ_succ Function.mt Finset.mem_of_mem_filter Finset.filter_cons Finset.card_cons Finset.filter_map Finset.card_map
card_filter_univ_succ' 📖	mathematical	—	Finset.card Finset.filter Finset.univ fintype	—	card_filter_univ_succ add_comm zero_add
card_filter_val_lt 📖	mathematical	—	Finset.card Finset.filter Finset.univ fintype	—	Finset.card_map Finset.map_filter' Finset.filter.congr_simp map_valEmbedding_univ Finset.Iio_filter_lt inf_of_le_left Nat.card_Iio
lt_card_filter_univ_iff_apply_of_imp 📖	mathematical	—	Finset.card Finset.filter Finset.univ fintype	—	card_Iio Finset.card_le_card Finset.eq_of_subset_of_card_le card_filter_val_lt
map_valEmbedding_univ 📖	mathematical	—	Finset.map valEmbedding Finset.univ fintype Finset.Iio Nat.instPreorder LocallyFiniteOrder.toLocallyFiniteOrderBot Nat.instOrderBot Nat.instLocallyFiniteOrder	—	Finset.ext Function.Surjective.exists OrderIso.surjective

Finset

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
image_fin_univ 📖	mathematical	—	image univ Fin.fintype range	—	ext
sup_fin_univ 📖	mathematical	—	sup univ Fin.fintype range	—	image_fin_univ sup_image

---

← Back to Index