Disjointed for functions on a SuccAddOrder

This file contains material excised from Mathlib/Order/Disjointed.lean to avoid import dependencies from Mathlib.Algebra.Order into Mathlib.Order.

TODO

Find a useful statement of disjointedRec_succ.

theorem disjointed_add_one {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [LinearOrder ι] [LocallyFiniteOrderBot ι] [Add ι] [One ι] [SuccAddOrder ι] [NoMaxOrder ι] (f : ι → α) (i : ι) : disjointed f (i + 1) = f (i + 1) \ (partialSups f) i

theorem partialSups_add_one_eq_sup_disjointed {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [LinearOrder ι] [LocallyFiniteOrderBot ι] [Add ι] [One ι] [SuccAddOrder ι] (f : ι → α) (i : ι) : (partialSups f) (i + 1) = (partialSups f) i ⊔ disjointed f (i + 1)

theorem Monotone.disjointed_add_one_sup {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [LinearOrder ι] [LocallyFiniteOrderBot ι] [Add ι] [One ι] [SuccAddOrder ι] {f : ι → α} (hf : Monotone f) (i : ι) : disjointed f (i + 1) ⊔ f i = f (i + 1)

theorem Monotone.disjointed_add_one {α : Type u_1} {ι : Type u_2} [GeneralizedBooleanAlgebra α] [LinearOrder ι] [LocallyFiniteOrderBot ι] [Add ι] [One ι] [SuccAddOrder ι] [NoMaxOrder ι] {f : ι → α} (hf : Monotone f) (i : ι) : disjointed f (i + 1) = f (i + 1) \ f i

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

A recursion principle for disjointed. To construct / define something for disjointed f i, it's enough to construct / define it for f n and to able to extend through diffs.

Note that this version allows an arbitrary Sort*, but requires the domain to be Nat, while the root-level disjointedRec allows more general domains but requires p to be Prop-valued.

Equations

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

@[simp]

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