Theorems · Theorem · order theory

DFinsupp.lex_lt_of_lt_of_preorder

∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : (i : ι) → Preorder (α i)] (r : ι → ι → Prop)
  [IsStrictOrder ι r] {x y : Π₀ (i : ι), α i}, x < y → ∃ i, (∀ (j : ι), r j i → x j ≤ y j ∧ y j ≤ x j) ∧ x i < y i

Defined in

Mathlib.Data.DFinsupp.Lex

Cited by

3 results in Mathlib

Foundations

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

Assumes

ZeroPreorderIsStrictOrder