Theorems · Theorem · order theory

Pi.toLex_update_lt_self_iff

∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] {x : (i : ι) → β i} {i : ι} {a : β i}
  [inst_1 : (i : ι) → PartialOrder (β i)] [WellFoundedLT ι], toLex (Function.update x i a) < toLex x ↔ a < x i

Defined in

Mathlib.Order.PiLex

Cited by

1 results in Mathlib

Foundations

Depth 21 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderPartialOrderWellFoundedLT