Lex

📁 Source: Mathlib/Data/Sigma/Lex.lean

Statistics

Metric	Count
Definitions decidable, Lex, decidable	3
Theorems mono, mono_left, mono_right, lex_iff, mono, mono_left, mono_right, instAntisymmLexOfAsymm, instIrreflLex, instIsTransLex, instReflLex, instSymmLex, instTotalLexOfTrichotomous, instTrichotomousLex, lex_iff, lex_swap	16
Total	19

PSigma

Theorems

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

PSigma.Lex

Definitions

Name	Category	Theorems
decidable 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	—	—	—	—	—
mono_left 📖	—	—	—	—	mono
mono_right 📖	—	—	—	—	mono

Sigma

Definitions

Name	Category	Theorems
Lex 📖	CompData	14 math math: Set.WellFoundedOn.sigma_lex_of_wellFoundedOn_fiber, instTotalLexOfTrichotomous, instIsTransLex, lex_iff, instReflLex, instTrichotomousLex, instAntisymmLexOfAsymm, instIrreflLex, Lex.mono_left, Lex.mono, lex_swap, WellFounded.sigma_lex_of_wellFoundedOn_fiber, instSymmLex, Lex.mono_right

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAntisymmLexOfAsymm 📖	mathematical	—	Lex	—	asymm irrefl antisymm
instIrreflLex 📖	mathematical	—	Lex	—	irrefl
instIsTransLex 📖	mathematical	IsTrans	IsTrans Lex	—	trans
instReflLex 📖	mathematical	—	Lex	—	refl
instSymmLex 📖	mathematical	—	Lex	—	symm
instTotalLexOfTrichotomous 📖	mathematical	—	Lex	—	trichotomous_of total_of
instTrichotomousLex 📖	mathematical	—	Lex	—	trichotomous_of
lex_iff 📖	mathematical	—	Lex	—	—
lex_swap 📖	mathematical	—	Lex Function.swap	—	—

Sigma.Lex

Definitions

Name	Category	Theorems
decidable 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mono 📖	mathematical	Sigma.Lex	Sigma.Lex	—	—
mono_left 📖	mathematical	Sigma.Lex	Sigma.Lex	—	mono
mono_right 📖	mathematical	Sigma.Lex	Sigma.Lex	—	mono

---

← Back to Index