Theorems · Theorem · order theory

Finset.intervalGapsWithin_fst_le_snd

∀ {α : Type u_1} [inst : LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (j : ℕ) {a b : α},
  a ≤ b →
    (∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b) →
      ((↑F).PairwiseDisjoint fun z => Set.Icc z.1 z.2) →
        (F.intervalGapsWithin h a b ↑j).1 ≤ (F.intervalGapsWithin h a b ↑j).2

Defined in

Mathlib.Order.Interval.Finset.Gaps

Cited by

1 results in Mathlib

Foundations

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

Assumes

LinearOrder