Theorems · Theorem · order theory

Finset.intervalGapsWithin_succ_fst_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.succ).1 = ((F.orderEmbOfFin h) ⟨j, hj⟩).2

Defined in

Mathlib.Order.Interval.Finset.Gaps

Cited by

4 results in Mathlib

Foundations

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

Assumes

LinearOrder