Mathlib Map

Theorems · Theorem · order theory

ofLex_toLex

∀ {α : Type u_1} (a : α), ofLex (toLex a) = a
Defined in
Mathlib.Order.Lex
Cited by
5 results in Mathlib
Foundations
Depth 14 from the axioms · uses Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

HahnEmbedding.Partial.orderTop_eq_archimedeanClassMk · cited by 3Partial.orderTop_eq_archi…MvPolynomial.supDegree_esymm · cited by 1MvPolynomial.supDegree_es…HahnEmbedding.Partial.apply_of_mem_stratum · cited by 1Partial.apply_of_mem_stra…HahnEmbedding.Seed.truncLT_mem_range_baseEmbedding · cited by 1Seed.truncLT_mem_range_ba…HahnEmbedding.Partial.truncLT_eval_mem_range_extendFun · cited by 1Partial.truncLT_eval_mem_…DFunLike.coe · cited by 62936DFunLike.coeEquiv · cited by 8337EquivLex · cited by 370LextoLex · cited by 195toLexofLex · cited by 127ofLexofLex_toLexCITED BYCITES

Cites5

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • DFunLike.coestatement · cited by 62,936
  • Equivstatement · cited by 8,337
  • Lexstatement · cited by 370
  • toLexstatement · cited by 195
  • ofLexstatement · cited by 127

Cited by5

Results whose statement or proof uses this declaration.