mathlib documentation

order.disjointed

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 #

We also provide set notation variants of some lemmas.

TODO #

Find a useful statement of disjointed_rec_succ.

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

source
def disjointed {α : Type u_1} [generalized_boolean_algebra α] (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
source
@[simp]
theorem disjointed_zero {α : Type u_1} [generalized_boolean_algebra α] (f : ℕ → α) :
disjointed f 0 = f 0
source
theorem disjointed_succ {α : Type u_1} [generalized_boolean_algebra α] (f : ℕ → α) (n : ℕ) :
disjointed f (n + 1) = f (n + 1) \ ⇑(partial_sups f) n
source
theorem disjointed_le_id {α : Type u_1} [generalized_boolean_algebra α] :
disjointed ≤ id
source
theorem disjointed_le {α : Type u_1} [generalized_boolean_algebra α] (f : ℕ → α) :
disjointed f ≤ f
source
theorem disjoint_disjointed {α : Type u_1} [generalized_boolean_algebra α] (f : ℕ → α) :
pairwise (disjoint on disjointed f)
source
def disjointed_rec {α : Type u_1} [generalized_boolean_algebra α] {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
source
@[simp]
theorem disjointed_rec_zero {α : Type u_1} [generalized_boolean_algebra α] {f : ℕ → α} {p : α → Sort u_2} (hdiff : Π ⦃t : α⦄ ⦃i : ℕ⦄, p t → p (t \ f i)) (h₀ : p (f 0)) :
disjointed_rec hdiff h₀ = h₀
source
theorem monotone.disjointed_eq {α : Type u_1} [generalized_boolean_algebra α] {f : ℕ → α} (hf : monotone f) (n : ℕ) :
disjointed f (n + 1) = f (n + 1) \ f n
source
@[simp]
theorem partial_sups_disjointed {α : Type u_1} [generalized_boolean_algebra α] (f : ℕ → α) :
partial_sups (disjointed f) = partial_sups f
source
theorem disjointed_unique {α : Type u_1} [generalized_boolean_algebra α] {f d : ℕ → α} (hdisj : pairwise (disjoint on d)) (hsups : partial_sups d = partial_sups f) :
d = disjointed f

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

source
theorem supr_disjointed {α : Type u_1} [complete_boolean_algebra α] (f : ℕ → α) :
(⨆ (n : ℕ), disjointed f n) = ⨆ (n : ℕ), f n
source
theorem disjointed_eq_inf_compl {α : Type u_1} [complete_boolean_algebra α] (f : ℕ → α) (n : ℕ) :
disjointed f n = f n ⊓ ⨅ (i : ℕ) (H : i < n), (f i)ᶜ

Set notation variants of lemmas #

source
theorem disjointed_subset {α : Type u_1} (f : ℕ → set α) (n : ℕ) :
disjointed f n ⊆ f n
source
theorem Union_disjointed {α : Type u_1} {f : ℕ → set α} :
(⋃ (n : ℕ), disjointed f n) = ⋃ (n : ℕ), f n
source
theorem disjointed_eq_inter_compl {α : Type u_1} (f : ℕ → set α) (n : ℕ) :
disjointed f n = f n ∩ ⋂ (i : ℕ) (H : i < n), (f i)ᶜ
source
theorem preimage_find_eq_disjointed {α : Type u_1} (s : ℕ → set α) (H : ∀ (x : α), ∃ (n : ℕ), x ∈ s n) [Π (x : α) (n : ℕ), decidable (x ∈ s n)] (n : ℕ) :
(λ (x : α), nat.find _) ⁻¹' {n} = disjointed s n