Finset

📁 Source: Mathlib/Logic/Equiv/Finset.lean

Statistics

Metric	Count
Definitions finset, lower', raise', raise'Finset, fintypeEquivFin, sortedUniv, encodable	7
Theorems isChain_cons_raise', isChain_cons_raise'_of_lt, isChain_raise', lower_raise', raise'_chain, raise'_sorted, raise_lower', length_sortedUniv, mem_sortedUniv, sortedUniv_nodup, sortedUniv_toFinset	11
Total	18

Denumerable

Definitions

Name	Category	Theorems
finset 📖	CompOp	—
lower' 📖	CompOp	2 math math: lower_raise', raise_lower'
raise' 📖	CompOp	7 math math: lower_raise', isChain_raise', isChain_cons_raise', isChain_cons_raise'_of_lt, raise'_sorted, raise_lower', raise'_chain
raise'Finset 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isChain_cons_raise' 📖	mathematical	—	raise'	—	isChain_raise'
isChain_cons_raise'_of_lt 📖	mathematical	—	raise'	—	raise'.eq_def
isChain_raise' 📖	mathematical	—	raise'	—	—
lower_raise' 📖	mathematical	—	lower' raise'	—	—
raise'_chain 📖	mathematical	—	raise'	—	isChain_cons_raise'_of_lt
raise'_sorted 📖	mathematical	—	List.SortedLT Nat.instPreorder raise'	—	List.IsChain.sortedLT isChain_raise'
raise_lower' 📖	mathematical	List.SortedLT Nat.instPreorder	raise' lower'	—	List.SortedLT.pairwise List.Pairwise.sortedLT

Encodable

Definitions

Name	Category	Theorems
fintypeEquivFin 📖	CompOp	—
sortedUniv 📖	CompOp	4 math math: mem_sortedUniv, sortedUniv_toFinset, sortedUniv_nodup, length_sortedUniv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
length_sortedUniv 📖	mathematical	—	sortedUniv Fintype.card	—	Finset.length_sort instAntisymmPreimageNatCoeEmbeddingEncode'Le instTotalPreimageNatCoeEmbeddingEncode'Le
mem_sortedUniv 📖	mathematical	—	sortedUniv	—	instAntisymmPreimageNatCoeEmbeddingEncode'Le instTotalPreimageNatCoeEmbeddingEncode'Le Finset.mem_sort Finset.mem_univ
sortedUniv_nodup 📖	mathematical	—	sortedUniv	—	Finset.sort_nodup instAntisymmPreimageNatCoeEmbeddingEncode'Le instTotalPreimageNatCoeEmbeddingEncode'Le
sortedUniv_toFinset 📖	mathematical	—	List.toFinset sortedUniv Finset.univ	—	Finset.sort_toFinset instAntisymmPreimageNatCoeEmbeddingEncode'Le instTotalPreimageNatCoeEmbeddingEncode'Le

Finset

Definitions

Name	Category	Theorems
encodable 📖	CompOp	—

---

← Back to Index