Making a sequence disjoint

This file defines the way to make a sequence of sets - or, more generally, a map from a partially ordered type ι into a (generalized) Boolean algebra α - into a pairwise disjoint sequence 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 map sending i to f i \ (⨆ j < i, f j). We require the index type to be a LocallyFiniteOrderBot to ensure that the supremum is well defined.
• 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.
• Fintype.sup_disjointed (for finite ι) or iSup_disjointed (for complete α): disjointed f has the same supremum as f. Limiting case of partialSups_disjointed.
• Fintype.exists_disjointed_le: for any finite family f : ι → α, there exists a pairwise disjoint family g : ι → α which is bounded above by f and has the same supremum. This is an analogue of disjointed for arbitrary finite index types (but without any uniqueness).

We also provide set notation variants of some lemmas.

def disjointed {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → α) (i : ι) : α

The function mapping i to f i \ (⨆ j < i, f j). When ι is a partial order, this is the unique function g having the same partialSups as f and such that g i and g j are disjoint whenever i < j.

Equations

• disjointed f i = f i \ (Finset.Iio i).sup f

theorem disjointed_apply {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → α) (i : ι) : disjointed f i = f i \ (Finset.Iio i).sup f

theorem disjointed_of_isMin {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → α) {i : ι} (hn : IsMin i) : disjointed f i = f i

@[simp]

theorem disjointed_bot {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [Preorder ι] [LocallyFiniteOrderBot ι] [OrderBot ι] (f : ι → α) : disjointed f ⊥ = f ⊥

theorem disjointed_le_id {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [Preorder ι] [LocallyFiniteOrderBot ι] : disjointed ≤ id

theorem disjointed_le {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → α) : disjointed f ≤ f

theorem disjoint_disjointed_of_lt {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → α) {i j : ι} (h : i < j) : Disjoint (disjointed f i) (disjointed f j)

theorem disjointed_eq_self {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [Preorder ι] [LocallyFiniteOrderBot ι] {f : ι → α} {i : ι} (hf : ∀ j < i, Disjoint (f j) (f i)) : disjointed f i = f i

theorem disjointedRec {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [Preorder ι] [LocallyFiniteOrderBot ι] {f : ι → α} {p : α → Prop} (hdiff : ∀ ⦃t : α⦄ ⦃i : ι⦄, p t → p (t \ f i)) ⦃i : ι⦄ : p (f i) → p (disjointed f i)

An induction principle for disjointed. To prove something about disjointed f i, it's enough to prove it for f i and being able to extend through diffs.

@[simp]

theorem partialSups_disjointed {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [PartialOrder ι] [LocallyFiniteOrderBot ι] (f : ι → α) : partialSups (disjointed f) = partialSups f

theorem Fintype.sup_disjointed {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [PartialOrder ι] [LocallyFiniteOrderBot ι] [Fintype ι] (f : ι → α) : Finset.univ.sup (disjointed f) = Finset.univ.sup f

theorem disjointed_partialSups {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [PartialOrder ι] [LocallyFiniteOrderBot ι] (f : ι → α) : disjointed ⇑(partialSups f) = disjointed f

theorem disjointed_unique {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [PartialOrder ι] [LocallyFiniteOrderBot ι] {f d : ι → α} (hdisj : ∀ {i j : ι}, i < j → Disjoint (d i) (d j)) (hsups : partialSups d = partialSups f) : d = disjointed f

disjointed f is the unique map d : ι → α such that d has the same partial sups as f, and d i and d j are disjoint whenever i < j.

Linear orders

theorem disjoint_disjointed {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [LinearOrder ι] [LocallyFiniteOrderBot ι] (f : ι → α) : Pairwise (Function.onFun Disjoint (disjointed f))

theorem disjointed_unique' {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [LinearOrder ι] [LocallyFiniteOrderBot ι] {f d : ι → α} (hdisj : Pairwise (Function.onFun Disjoint 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 disjointed_succ {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [LinearOrder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] (f : ι → α) {i : ι} (hi : ¬IsMax i) : disjointed f (Order.succ i) = f (Order.succ i) \ (partialSups f) i

theorem Monotone.disjointed_succ {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [LinearOrder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] {f : ι → α} (hf : Monotone f) {i : ι} (hn : ¬IsMax i) : disjointed f (Order.succ i) = f (Order.succ i) \ f i

theorem Monotone.disjointed_succ_sup {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [LinearOrder ι] [LocallyFiniteOrderBot ι] [SuccOrder ι] {f : ι → α} (hf : Monotone f) (i : ι) : disjointed f (Order.succ i) ⊔ f i = f (Order.succ i)

Note this lemma does not require ¬IsMax i, unlike disjointed_succ.

Functions on an arbitrary fintype

theorem Fintype.exists_disjointed_le {α : Type u_1} [GeneralizedBooleanAlgebra α] {ι : Type u_3} [Fintype ι] (f : ι → α) : ∃ g ≤ f, Finset.univ.sup g = Finset.univ.sup f ∧ Pairwise (Function.onFun Disjoint g)

For any finite family of elements f : ι → α, we can find a pairwise-disjoint family g bounded above by f and having the same supremum. This is non-canonical, depending on an arbitrary choice of ordering of ι.

Complete Boolean algebras

theorem iSup_disjointed {α : Type u_1} {ι : Type u_2} [CompleteBooleanAlgebra α] [PartialOrder ι] [LocallyFiniteOrderBot ι] (f : ι → α) : ⨆ (i : ι), disjointed f i = ⨆ (i : ι), f i

theorem disjointed_eq_inf_compl {α : Type u_1} {ι : Type u_2} [CompleteBooleanAlgebra α] [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → α) (i : ι) : disjointed f i = f i ⊓ ⨅ (j : ι), ⨅ (_ : j < i), (f j)ᶜ

Lemmas specific to set-valued functions

theorem disjointed_subset {α : Type u_1} {ι : Type u_2} [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → Set α) (i : ι) : disjointed f i ⊆ f i

theorem iUnion_disjointed {α : Type u_1} {ι : Type u_2} [PartialOrder ι] [LocallyFiniteOrderBot ι] {f : ι → Set α} : ⋃ (i : ι), disjointed f i = ⋃ (i : ι), f i

theorem disjointed_eq_inter_compl {α : Type u_1} {ι : Type u_2} [Preorder ι] [LocallyFiniteOrderBot ι] (f : ι → Set α) (i : ι) : disjointed f i = f i ∩ ⋂ (j : ι), ⋂ (_ : j < i), (f j)ᶜ

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

Functions on ℕ

(See also Mathlib/Algebra/Order/Disjointed.lean for results with more algebra pre-requisites.)

@[simp]

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