Mathlib Map

Theorems · Theorem · order theory

Pi.lex_iff_of_unique

∀ {ι : Type u_1} {β : ι → Type u_2} [inst : Unique ι] [inst_1 : (i : ι) → LT (β i)] {r : ι → ι → Prop} [Std.Irrefl r]
  {x y : (i : ι) → β i}, Pi.Lex r (fun {i} x1 x2 => x1 < x2) x y ↔ x default < y default
Defined in
Mathlib.Order.PiLex
Cited by
4 results in Mathlib
Foundations
Depth 7 from the axioms · uses propext, Quot.sound
Assumes
UniqueLTStd.Irrefl
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

DFinsupp.lex_iff_of_unique · cited by 2DFinsupp.lex_iff_of_uniqueFinsupp.lex_iff_of_unique · cited by 1Finsupp.lex_iff_of_uniquePi.Lex.lt_iff_of_unique · cited by 0Lex.lt_iff_of_uniquePi.Colex.lt_iff_of_unique · cited by 0Colex.lt_iff_of_uniqueUnique · cited by 400UniquePi.Lex · cited by 11Pi.LexPi.lex_iff_of_uniqueCITED BYCITES

Cites2

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

  • Uniquestatement and proof · cited by 400
  • Pi.Lexstatement · cited by 11

Cited by4

Results whose statement or proof uses this declaration.