Gaps of disjoint closed intervals

This file defines Finset.intervalGapsWithin that computes the complement of the union of a collection of pairwise disjoint subintervals of [a, b].

If LinearOrder α, F is a finite subset of α × α such that for any (x, y) ∈ F, a ≤ x ≤ y ≤ b and all such [x, y]'s are pairwise disjoint, h is a proof of F.card = k, i is in Fin (k + 1), we order F from left to right 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.

Technically, the definition F.intervalGapsWithin a b does not require F to be pairwise disjoint or endpoints to be within [a, b] or even require that a ≤ b, but it makes the most sense if they are actually satisfied. If they are actually satisfied, then we show that

• Finset.intervalGapsWithin_mapsTo, Finset.intervalGapsWithin_injective, Finset.intervalGapsWithin_surjOn: (fun j ↦ ((F.intervalGapsWithin h a b j.castSucc).2, (F.intervalGapsWithin h a b j.succ).1)) is a bijection between Set.Iio k and F.
• Finset.intervalGapsWithin_le_fst, Finset.intervalGapsWithin_snd_le, Finset.intervalGapsWithin_fst_le_snd: [(F.intervalGapsWithin h a b j).1, (F.intervalGapsWithin h a b j).2] is indeed a subinterval of [a, b] when j < k.
• Finset.intervalGapsWithin_pairwiseDisjoint_Ioc: the half-closed intervals [(F.intervalGapsWithin h a b j).1, (F.intervalGapsWithin h a b j).2) are pairwise disjoint for j < k + 1.

noncomputable def Finset.intervalGapsWithin {α : Type u_1} [LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (a b : α) (i : 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.

noncomputable def Finset.intervalGapsWithin.fst {α : Type u_1} [LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (a : α) (i : Fin (k + 1)) : α

The first coordinate of F.intervalGapsWithin h a b i is a if i = 0, y (i - 1) otherwise.

noncomputable def Finset.intervalGapsWithin.snd {α : Type u_1} [LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (b : α) (i : Fin (k + 1)) : α

The second coordinate of F.intervalGapsWithin h a b i is b if i = k, x i otherwise.

@[simp]

theorem Finset.intervalGapsWithin_zero_fst {α : Type u_1} [LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (a b : α) : (F.intervalGapsWithin h a b 0).1 = a

theorem Finset.intervalGapsWithin_succ_fst_of_lt {α : Type u_1} [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

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

@[simp]

theorem Finset.intervalGapsWithin_last_snd {α : Type u_1} [LinearOrder α] (F : Finset (α × α)) {k : ℕ} (h : F.card = k) (a b : α) : (F.intervalGapsWithin h a b (Fin.last k)).2 = b

theorem Finset.intervalGapsWithin_snd_of_lt {α : Type u_1} [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

theorem Finset.intervalGapsWithin_mapsTo {α : Type u_1} [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

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

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

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

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

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

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