Theorems · Definition · order theory
Finsupp.Lex
{α : Type u_1} → {N : Type u_2} → [inst : Zero N] → (α → α → Prop) → (N → N → Prop) → (α →₀ N) → (α →₀ N) → PropFinsupp.Lex r s is the lexicographic relation on α →₀ N, where α is ordered by r,
and N is ordered by s.
The type synonym Lex (α →₀ N) has an order given by Finsupp.Lex (· < ·) (· < ·).
- Defined in
- Mathlib.Data.Finsupp.Lex
- Cited by
- 11 results in Mathlib
- Foundations
- Depth 59 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Zero
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Finsuppstatement and proof · cited by 5,255
- Pi.Lexproof · cited by 11
Cited by12
Results whose statement or proof uses this declaration.
- Finsupp.lex_eq_invImage_dfinsupp_lexstatement · cited by 2
- Finsupp.DegLexproof · cited by 2
- Finsupp.lex_iff_of_uniquestatement · cited by 1
- Finsupp.Lex.accstatement · cited by 1
- Finsupp.Lex.wellFounded'statement · cited by 1
- Finsupp.Lex.wellFounded_of_finitestatement · cited by 1
- Finsupp.lex_defstatement · cited by 0
- Relation.cutExpand_le_invImage_lexstatement · cited by 0
- Pi.lex_eq_finsupp_lexstatement · cited by 0
- Finsupp.Lex.wellFoundedstatement · cited by 0
- Finsupp.degLex_defstatement · cited by 0
- Finsupp.DegLex.wellFoundedproof · cited by 0