Theorems · Theorem · order theory

Finset.intervalGapsWithin_mapsTo

∀ {α : Type u_1} [inst : LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (a b : α),
  Set.MapsTo (fun j => ((F.intervalGapsWithin h a b ↑j).2, (F.intervalGapsWithin h a b ↑j.succ).1)) (Set.Iio k) ↑F

Defined in

Mathlib.Order.Interval.Finset.Gaps

Cited by

6 results in Mathlib

Foundations

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

Assumes

LinearOrder