Documentation

Mathlib.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 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
Instances For
    @[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 : α) :
    theorem disjoint_disjointed {α : Type u_1} [GeneralizedBooleanAlgebra α] (f : α) :
    Pairwise (Disjoint on disjointed f)
    def disjointedRec {α : Type u_1} [GeneralizedBooleanAlgebra α] {f : α} {p : αSort u_3} (hdiff : t : α⦄ → i : ⦄ → p tp (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
    Instances For
      @[simp]
      theorem disjointedRec_zero {α : Type u_1} [GeneralizedBooleanAlgebra α] {f : α} {p : αSort u_3} (hdiff : t : α⦄ → i : ⦄ → p tp (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)
      theorem disjointed_unique {α : Type u_1} [GeneralizedBooleanAlgebra α] {f : α} {d : α} (hdisj : Pairwise (Disjoint on d)) (hsups : partialSups d = partialSups 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