Theorems · Theorem · order theory

Pi.toColex_update_lt_self_iff

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

Defined in

Mathlib.Order.PiLex

Cited by

0 results in Mathlib

Foundations

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

Assumes

LinearOrderPartialOrderWellFoundedGT