Fin

📁 Source: SDG/Axiom/Fin.lean

Statistics

Metric	Count
Definitions fintype	1
Theorems existing, Fintype_prod_eq_prod, Fintype_sum_eq_sum, prod_castLe_of_eq_one, prod_cons, prod_cons_one, prod_natAdd_zero, prod_ofFn, prod_snoc, prod_snoc_one, prod_trunc, prod_univ_add, prod_univ_def, prod_univ_one, prod_univ_succ, prod_univ_succAbove_last, prod_univ_two, prod_univ_zero, sum_castLe_of_eq_zero, sum_cons, sum_cons_zero, sum_natAdd_zero, sum_ofFn, sum_snoc, sum_snoc_zero, sum_trunc, sum_univ_add, sum_univ_def, sum_univ_one, sum_univ_succ, sum_univ_succAbove_last, sum_univ_two, sum_univ_zero, univ_def, univ_val_map, nodup_finRange, nodup_range, nodup_range', pairwise_le_range', pairwise_lt_range'	40
Total	41

Fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
existing 📖	—	—	—	—	—

SDG.Fin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
Fintype_prod_eq_prod 📖	mathematical	—	SDG.List.Fin.fintype	—	prod_univ_def
Fintype_sum_eq_sum 📖	mathematical	—	SDG.List.Fin.fintype	—	Fin.existing sum_univ_def
prod_castLe_of_eq_one 📖	mathematical	—	SDG.List.Fin.fintype	—	prod_univ_add
prod_cons 📖	mathematical	—	SDG.List.Fin.fintype	—	prod_univ_succ
prod_cons_one 📖	mathematical	—	SDG.List.Fin.fintype	—	prod_cons
prod_natAdd_zero 📖	mathematical	—	SDG.List.Fin.fintype	—	prod_univ_succ
prod_ofFn 📖	mathematical	—	SDG.List.Fin.fintype	—	univ_val_map
prod_snoc 📖	mathematical	—	SDG.List.Fin.fintype	—	prod_univ_succAbove_last
prod_snoc_one 📖	mathematical	—	SDG.List.Fin.fintype	—	prod_snoc
prod_trunc 📖	mathematical	—	SDG.List.Fin.fintype	—	prod_univ_add
prod_univ_add 📖	mathematical	—	SDG.List.Fin.fintype	—	prod_natAdd_zero prod_univ_succAbove_last
prod_univ_def 📖	mathematical	—	SDG.List.Fin.fintype	—	prod_ofFn
prod_univ_one 📖	mathematical	—	SDG.List.Fin.fintype	—	prod_univ_succ
prod_univ_succ 📖	mathematical	—	SDG.List.Fin.fintype	—	Fintype_prod_eq_prod
prod_univ_succAbove_last 📖	mathematical	—	SDG.List.Fin.fintype	—	Fintype_prod_eq_prod
prod_univ_two 📖	mathematical	—	SDG.List.Fin.fintype	—	prod_univ_succ prod_univ_one
prod_univ_zero 📖	mathematical	—	SDG.List.Fin.fintype	—	—
sum_castLe_of_eq_zero 📖	mathematical	—	SDG.List.Fin.fintype	—	sum_univ_add
sum_cons 📖	mathematical	—	SDG.List.Fin.fintype	—	sum_univ_succ
sum_cons_zero 📖	mathematical	—	SDG.List.Fin.fintype	—	sum_cons
sum_natAdd_zero 📖	mathematical	—	SDG.List.Fin.fintype	—	sum_univ_succ
sum_ofFn 📖	mathematical	—	SDG.List.Fin.fintype	—	univ_val_map
sum_snoc 📖	mathematical	—	SDG.List.Fin.fintype	—	sum_univ_succAbove_last
sum_snoc_zero 📖	mathematical	—	SDG.List.Fin.fintype	—	sum_snoc
sum_trunc 📖	mathematical	—	SDG.List.Fin.fintype	—	sum_univ_add
sum_univ_add 📖	mathematical	—	SDG.List.Fin.fintype	—	sum_natAdd_zero sum_univ_succAbove_last
sum_univ_def 📖	mathematical	—	SDG.List.Fin.fintype	—	sum_ofFn
sum_univ_one 📖	mathematical	—	SDG.List.Fin.fintype	—	sum_univ_succ
sum_univ_succ 📖	mathematical	—	SDG.List.Fin.fintype	—	Fintype_sum_eq_sum
sum_univ_succAbove_last 📖	mathematical	—	SDG.List.Fin.fintype	—	Fintype_sum_eq_sum Fin.existing
sum_univ_two 📖	mathematical	—	SDG.List.Fin.fintype	—	sum_univ_succ sum_univ_one
sum_univ_zero 📖	mathematical	—	SDG.List.Fin.fintype	—	—
univ_def 📖	mathematical	—	SDG.List.Fin.fintype SDG.List.nodup_finRange	—	—
univ_val_map 📖	mathematical	—	SDG.List.Fin.fintype	—	—

SDG.List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
nodup_finRange 📖	—	—	—	—	nodup_range
nodup_range 📖	—	—	—	—	—
nodup_range' 📖	—	—	—	—	pairwise_lt_range'
pairwise_le_range' 📖	—	—	—	—	—
pairwise_lt_range' 📖	—	—	—	—	—

SDG.List.Fin

Definitions

Name	Category	Theorems
fintype 📖	CompOp	36 math math: SDG.Fin.Fintype_sum_eq_sum, SDG.Fin.prod_univ_succAbove_last, SDG.Fin.univ_def, SDG.Fin.sum_cons_zero, SDG.Fin.prod_univ_add, SDG.Fin.sum_trunc, SDG.Fin.sum_ofFn, SDG.Fin.prod_snoc_one, SDG.Fin.univ_val_map, SDG.Fin.prod_cons_one, SDG.Fin.sum_univ_def, SDG.mem_D_sum_pow, SDG.Fin.sum_univ_zero, SDG.Fin.prod_cons, SDG.Fin.sum_univ_one, SDG.Fin.sum_univ_two, SDG.Fin.prod_univ_zero, SDG.Fin.prod_univ_def, SDG.Fin.sum_snoc, SDG.Fin.prod_trunc, SDG.Fin.prod_ofFn, SDG.Fin.sum_univ_add, SDG.Fin.prod_natAdd_zero, SDG.Fin.sum_snoc_zero, SDG.Fin.sum_castLe_of_eq_zero, SDG.Fin.sum_univ_succ, SDG.Fin.prod_univ_one, SDG.Fin.sum_natAdd_zero, SDG.mem_D_sum_pow_succ, SDG.Fin.sum_cons, SDG.Fin.prod_univ_two, SDG.Fin.Fintype_prod_eq_prod, SDG.Fin.prod_castLe_of_eq_one, SDG.Fin.sum_univ_succAbove_last, SDG.Fin.prod_univ_succ, SDG.Fin.prod_snoc

---

← Back to Index