Theorems · Theorem · order theory

Finset.intervalGapsWithin_snd_of_lt

∀ {α : Type u_1} [inst : LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (a b : α) (j : ℕ) (hj : j < k),
  (F.intervalGapsWithin h a b ↑j).2 = ((F.orderEmbOfFin h) ⟨j, hj⟩).1

Defined in

Mathlib.Order.Interval.Finset.Gaps

Cited by

5 results in Mathlib

Foundations

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

Assumes

LinearOrder