Consecutive differences of sets

This file defines the way to make a sequence of elements into a sequence of disjoint elements with the same partial sups.

For a sequence f : ℕ → α, this new sequence will be f 0, f 1 \ f 0, f 2 \ (f 0 ⊔ f 1). It is actually unique, as disjointed_unique shows.

Main declarations

• disjointed f: The sequence f 0, f 1 \ f 0, f 2 \ (f 0 ⊔ f 1), ....
• partialSups_disjointed: disjointed f has the same partial sups as f.
• disjoint_disjointed: The elements of disjointed f are pairwise disjoint.
• disjointed_unique: disjointed f is the only pairwise disjoint sequence having the same partial sups as f.
• iSup_disjointed: disjointed f has the same supremum as f. Limiting case of partialSups_disjointed.

We also provide set notation variants of some lemmas.

TODO

Find a useful statement of disjointedRec_succ.

One could generalize disjointed to any locally finite bot preorder domain, in place of ℕ. Related to the TODO in the module docstring of Mathlib.Order.PartialSups.

def disjointed {α : Type u_1} [GeneralizedBooleanAlgebra α] (f : ℕ → α) : ℕ → α

If f : ℕ → α is a sequence of elements, then disjointed f is the sequence formed by subtracting each element from the nexts. This is the unique disjoint sequence whose partial sups are the same as the original sequence.

Equations

• disjointed f 0 = f 0
• disjointed f n.succ = f (n + 1) \ (partialSups f) n

@[simp]

theorem disjointed_zero {α : Type u_1} [GeneralizedBooleanAlgebra α] (f : ℕ → α) : disjointed f 0 = f 0

theorem disjointed_succ {α : Type u_1} [GeneralizedBooleanAlgebra α] (f : ℕ → α) (n : ℕ) : disjointed f (n + 1) = f (n + 1) \ (partialSups f) n

theorem disjointed_le_id {α : Type u_1} [GeneralizedBooleanAlgebra α] : disjointed ≤ id

theorem disjointed_le {α : Type u_1} [GeneralizedBooleanAlgebra α] (f : ℕ → α) : disjointed f ≤ f

theorem disjoint_disjointed {α : Type u_1} [GeneralizedBooleanAlgebra α] (f : ℕ → α) : Pairwise (Disjoint on disjointed f)

def disjointedRec {α : Type u_1} [GeneralizedBooleanAlgebra α] {f : ℕ → α} {p : α → Sort u_2} (hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)) ⦃n : ℕ⦄ : p (f n) → p (disjointed f n)

An induction principle for disjointed. To define/prove something on disjointed f n, it's enough to define/prove it for f n and being able to extend through diffs.

Equations

• disjointedRec hdiff = id
• disjointedRec hdiff = fun (h : p (f (n + 1))) => let_fun H := fun (k : ℕ) => Nat.recAux (hdiff h) (fun (k : ℕ) (ih : p (f (n + 1) \ (partialSups f) k)) => ⋯.mpr (⋯.mpr (hdiff ih))) k; H n

@[simp]

theorem disjointedRec_zero {α : Type u_1} [GeneralizedBooleanAlgebra α] {f : ℕ → α} {p : α → Sort u_2} (hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)) (h₀ : p (f 0)) : disjointedRec hdiff h₀ = h₀

theorem Monotone.disjointed_succ {α : Type u_1} [GeneralizedBooleanAlgebra α] {f : ℕ → α} (hf : Monotone f) (n : ℕ) : disjointed f (n + 1) = f (n + 1) \ f n

theorem Monotone.disjointed_succ_sup {α : Type u_1} [GeneralizedBooleanAlgebra α] {f : ℕ → α} (hf : Monotone f) (n : ℕ) : disjointed f (n + 1) ⊔ f n = f (n + 1)

@[simp]

theorem partialSups_disjointed {α : Type u_1} [GeneralizedBooleanAlgebra α] (f : ℕ → α) : partialSups (disjointed f) = partialSups f

theorem disjointed_unique {α : Type u_1} [GeneralizedBooleanAlgebra α] {f d : ℕ → α} (hdisj : Pairwise (Disjoint on d)) (hsups : partialSups d = partialSups f) : d = disjointed f

disjointed f is the unique sequence that is pairwise disjoint and has the same partial sups as f.

theorem iSup_disjointed {α : Type u_1} [CompleteBooleanAlgebra α] (f : ℕ → α) : ⨆ (n : ℕ), disjointed f n = ⨆ (n : ℕ), f n

theorem disjointed_eq_inf_compl {α : Type u_1} [CompleteBooleanAlgebra α] (f : ℕ → α) (n : ℕ) : disjointed f n = f n ⊓ ⨅ (i : ℕ), ⨅ (_ : i < n), (f i)ᶜ

Set notation variants of lemmas

theorem disjointed_subset {α : Type u_1} (f : ℕ → Set α) (n : ℕ) : disjointed f n ⊆ f n

theorem iUnion_disjointed {α : Type u_1} {f : ℕ → Set α} : ⋃ (n : ℕ), disjointed f n = ⋃ (n : ℕ), f n

theorem disjointed_eq_inter_compl {α : Type u_1} (f : ℕ → Set α) (n : ℕ) : disjointed f n = f n ∩ ⋂ (i : ℕ), ⋂ (_ : i < n), (f i)ᶜ

theorem preimage_find_eq_disjointed {α : Type u_1} (s : ℕ → Set α) (H : ∀ (x : α), ∃ (n : ℕ), x ∈ s n) [(x : α) → (n : ℕ) → Decidable (x ∈ s n)] (n : ℕ) : (fun (x : α) => Nat.find ⋯) ⁻¹' {n} = disjointed s n