Theorems · Definition · order theory

Finset.intervalGapsWithin

{α : Type u_1} → [LinearOrder α] → (F : Finset (α × α)) → {k : ℕ} → F.card = k → α → α → Fin (k + 1) → α × α

We order F in the lexicographic order as (x 0, y 0), ..., (x (k - 1), y (k - 1)). Then F.intervalGapsWithin h a b i is - (a, b) if 0 = i = k; - (a, x 0) if 0 = i < k; - (y (i - 1), x i) if 0 < i < k; - (y (i - 1), b) if 0 < i = k.

Defined in

Mathlib.Order.Interval.Finset.Gaps

Cited by

20 results in Mathlib

Foundations

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

Assumes

LinearOrder