Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+βCtrl+βto navigate, Ctrl+π±οΈto focus. On Mac, use Cmdinstead of Ctrl.
```/-
Authors: Johannes HΓΆlzl, YaΓ«l Dillies

! This file was ported from Lean 3 source module order.disjointed
! leanprover-community/mathlib commit f7fc89d5d5ff1db2d1242c7bb0e9062ce47ef47c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.PartialSups

/-!
# 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`.
-/

variable {Ξ±: Type ?u.5976Ξ± Ξ²: Type ?u.1032Ξ² : Type _: Type (?u.5976+1)Type _}

section GeneralizedBooleanAlgebra

variable [GeneralizedBooleanAlgebra: Type ?u.698 β Type ?u.698GeneralizedBooleanAlgebra Ξ±: Type ?u.8Ξ±]

/-- 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. -/
def disjointed: (β β Ξ±) β β β Ξ±disjointed (f: β β Ξ±f : β: Typeβ β Ξ±: Type ?u.17Ξ±) : β: Typeβ β Ξ±: Type ?u.17Ξ±
| 0: β0 => f: β β Ξ±f 0: ?m.530
| n: βn + 1 => f: β β Ξ±f (n: βn + 1: ?m.1541) \ partialSups: {Ξ± : Type ?u.190} β [inst : SemilatticeSup Ξ±] β (β β Ξ±) β β βo Ξ±partialSups f: β β Ξ±f n: βn
#align disjointed disjointed: {Ξ± : Type u_1} β [inst : GeneralizedBooleanAlgebra Ξ±] β (β β Ξ±) β β β Ξ±disjointed

@[simp]
theorem disjointed_zero: β {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β β Ξ±), disjointed f 0 = f 0disjointed_zero (f: β β Ξ±f : β: Typeβ β Ξ±: Type ?u.618Ξ±) : disjointed: {Ξ± : Type ?u.632} β [inst : GeneralizedBooleanAlgebra Ξ±] β (β β Ξ±) β β β Ξ±disjointed f: β β Ξ±f 0: ?m.6390 = f: β β Ξ±f 0: ?m.6540 :=
rfl: β {Ξ± : Sort ?u.659} {a : Ξ±}, a = arfl
#align disjointed_zero disjointed_zero: β {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β β Ξ±), disjointed f 0 = f 0disjointed_zero

theorem disjointed_succ: β (f : β β Ξ±) (n : β), disjointed f (n + 1) = f (n + 1) \ β(partialSups f) ndisjointed_succ (f: β β Ξ±f : β: Typeβ β Ξ±: Type ?u.692Ξ±) (n: βn : β: Typeβ) : disjointed: {Ξ± : Type ?u.708} β [inst : GeneralizedBooleanAlgebra Ξ±] β (β β Ξ±) β β β Ξ±disjointed f: β β Ξ±f (n: βn + 1: ?m.7181) = f: β β Ξ±f (n: βn + 1: ?m.7891) \ partialSups: {Ξ± : Type ?u.825} β [inst : SemilatticeSup Ξ±] β (β β Ξ±) β β βo Ξ±partialSups f: β β Ξ±f n: βn :=
rfl: β {Ξ± : Sort ?u.982} {a : Ξ±}, a = arfl
#align disjointed_succ disjointed_succ: β {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β β Ξ±) (n : β),
disjointed f (n + 1) = f (n + 1) \ β(partialSups f) ndisjointed_succ

theorem disjointed_le_id: β {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±], disjointed β€ iddisjointed_le_id : disjointed: {Ξ± : Type ?u.1039} β [inst : GeneralizedBooleanAlgebra Ξ±] β (β β Ξ±) β β β Ξ±disjointed β€ (id: {Ξ± : Sort ?u.1062} β Ξ± β Ξ±id : (β: Typeβ β Ξ±: Type ?u.1029Ξ±) β β: Typeβ β Ξ±: Type ?u.1029Ξ±) := byGoals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.1032instβ: GeneralizedBooleanAlgebra Ξ±disjointed β€ idrintro f: β β Ξ±f n: βnΞ±: Type u_1Ξ²: Type ?u.1032instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±n: βdisjointed f n β€ id f n
Ξ±: Type u_1Ξ²: Type ?u.1032instβ: GeneralizedBooleanAlgebra Ξ±disjointed β€ idcases n: βnΞ±: Type u_1Ξ²: Type ?u.1032instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±zerodisjointed f Nat.zero β€ id f Nat.zeroΞ±: Type u_1Ξ²: Type ?u.1032instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±nβ: βsuccdisjointed f (Nat.succ nβ) β€ id f (Nat.succ nβ)
Ξ±: Type u_1Ξ²: Type ?u.1032instβ: GeneralizedBooleanAlgebra Ξ±disjointed β€ idΒ·Ξ±: Type u_1Ξ²: Type ?u.1032instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±zerodisjointed f Nat.zero β€ id f Nat.zero Ξ±: Type u_1Ξ²: Type ?u.1032instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±zerodisjointed f Nat.zero β€ id f Nat.zeroΞ±: Type u_1Ξ²: Type ?u.1032instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±nβ: βsuccdisjointed f (Nat.succ nβ) β€ id f (Nat.succ nβ)rflGoals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.1032instβ: GeneralizedBooleanAlgebra Ξ±disjointed β€ idΒ·Ξ±: Type u_1Ξ²: Type ?u.1032instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±nβ: βsuccdisjointed f (Nat.succ nβ) β€ id f (Nat.succ nβ) Ξ±: Type u_1Ξ²: Type ?u.1032instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±nβ: βsuccdisjointed f (Nat.succ nβ) β€ id f (Nat.succ nβ)exact sdiff_le: β {Ξ± : Type ?u.2018} [inst : GeneralizedCoheytingAlgebra Ξ±] {a b : Ξ±}, a \ b β€ asdiff_leGoals accomplished! π
#align disjointed_le_id disjointed_le_id: β {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±], disjointed β€ iddisjointed_le_id

theorem disjointed_le: β {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β β Ξ±), disjointed f β€ fdisjointed_le (f: β β Ξ±f : β: Typeβ β Ξ±: Type ?u.2095Ξ±) : disjointed: {Ξ± : Type ?u.2109} β [inst : GeneralizedBooleanAlgebra Ξ±] β (β β Ξ±) β β β Ξ±disjointed f: β β Ξ±f β€ f: β β Ξ±f :=
disjointed_le_id: β {Ξ± : Type ?u.2522} [inst : GeneralizedBooleanAlgebra Ξ±], disjointed β€ iddisjointed_le_id f: β β Ξ±f
#align disjointed_le disjointed_le: β {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β β Ξ±), disjointed f β€ fdisjointed_le

theorem disjoint_disjointed: β (f : β β Ξ±), Pairwise (Disjoint on disjointed f)disjoint_disjointed (f: β β Ξ±f : β: Typeβ β Ξ±: Type ?u.2546Ξ±) : Pairwise: {Ξ± : Type ?u.2559} β (Ξ± β Ξ± β Prop) β PropPairwise (Disjoint: {Ξ± : Type ?u.2571} β [inst : PartialOrder Ξ±] β [inst : OrderBot Ξ±] β Ξ± β Ξ± β PropDisjoint on disjointed: {Ξ± : Type ?u.2732} β [inst : GeneralizedBooleanAlgebra Ξ±] β (β β Ξ±) β β β Ξ±disjointed f: β β Ξ±f) := byGoals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.2549instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±Pairwise (Disjoint on disjointed f)refine' (Symmetric.pairwise_on: β {Ξ± : Type ?u.3293} {ΞΉ : Type ?u.3292} {r : Ξ± β Ξ± β Prop} [inst : LinearOrder ΞΉ],
Symmetric r β β (f : ΞΉ β Ξ±), Pairwise (r on f) β β β¦m n : ΞΉβ¦, m < n β r (f m) (f n)Symmetric.pairwise_on Disjoint.symm: β {Ξ± : Type ?u.3298} [inst : PartialOrder Ξ±] [inst_1 : OrderBot Ξ±] β¦a b : Ξ±β¦, Disjoint a b β Disjoint b aDisjoint.symm _: ?m.3295 β ?m.3294_).2: β {a b : Prop}, (a β b) β b β a2 fun m: ?m.3526m n: ?m.3529n h: ?m.3532h => _: Disjoint (?m.3463 m) (?m.3463 n)_Ξ±: Type u_1Ξ²: Type ?u.2549instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±m, n: βh: m < nDisjoint (disjointed f m) (disjointed f n)
Ξ±: Type u_1Ξ²: Type ?u.2549instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±Pairwise (Disjoint on disjointed f)cases n: ?m.3529nΞ±: Type u_1Ξ²: Type ?u.2549instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±m: βh: m < Nat.zerozeroDisjoint (disjointed f m) (disjointed f Nat.zero)Ξ±: Type u_1Ξ²: Type ?u.2549instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±m, nβ: βh: m < Nat.succ nβsuccDisjoint (disjointed f m) (disjointed f (Nat.succ nβ))
Ξ±: Type u_1Ξ²: Type ?u.2549instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±Pairwise (Disjoint on disjointed f)Β·Ξ±: Type u_1Ξ²: Type ?u.2549instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±m: βh: m < Nat.zerozeroDisjoint (disjointed f m) (disjointed f Nat.zero) Ξ±: Type u_1Ξ²: Type ?u.2549instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±m: βh: m < Nat.zerozeroDisjoint (disjointed f m) (disjointed f Nat.zero)Ξ±: Type u_1Ξ²: Type ?u.2549instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±m, nβ: βh: m < Nat.succ nβsuccDisjoint (disjointed f m) (disjointed f (Nat.succ nβ))exact (Nat.not_lt_zero: β (n : β), Β¬n < 0Nat.not_lt_zero _: β_ h: m < Nat.zeroh).elim: β {C : Sort ?u.4144}, False β CelimGoals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.2549instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±Pairwise (Disjoint on disjointed f)exact
disjoint_sdiff_self_right: β {Ξ± : Type ?u.4148} {x y : Ξ±} [inst : GeneralizedBooleanAlgebra Ξ±], Disjoint x (y \ x)disjoint_sdiff_self_right.mono_left: β {Ξ± : Type ?u.4159} [inst : PartialOrder Ξ±] [inst_1 : OrderBot Ξ±] {a b c : Ξ±}, a β€ b β Disjoint b c β Disjoint a cmono_left
((disjointed_le: β {Ξ± : Type ?u.4257} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β β Ξ±), disjointed f β€ fdisjointed_le f: β β Ξ±f m: ?m.3526m).trans: β {Ξ± : Type ?u.4263} [inst : Preorder Ξ±] {a b c : Ξ±}, a β€ b β b β€ c β a β€ ctrans (le_partialSups_of_le: β {Ξ± : Type ?u.4561} [inst : SemilatticeSup Ξ±] (f : β β Ξ±) {m n : β}, m β€ n β f m β€ β(partialSups f) nle_partialSups_of_le f: β β Ξ±f (Nat.lt_add_one_iff: β {a b : β}, a < b + 1 β a β€ bNat.lt_add_one_iff.1: β {a b : Prop}, (a β b) β a β b1 h: m < Nat.succ nβh)))Goals accomplished! π
#align disjoint_disjointed disjoint_disjointed: β {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β β Ξ±), Pairwise (Disjoint on disjointed f)disjoint_disjointed

-- Porting note: `disjointedRec` had a change in universe level.
/-- 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. -/
def disjointedRec: {Ξ± : Type u_1} β
[inst : GeneralizedBooleanAlgebra Ξ±] β
{f : β β Ξ±} β {p : Ξ± β Sort u_2} β (β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)) β β¦n : ββ¦ β p (f n) β p (disjointed f n)disjointedRec {f: β β Ξ±f : β: Typeβ β Ξ±: Type ?u.4692Ξ±} {p: Ξ± β Sort ?u.4707p : Ξ±: Type ?u.4692Ξ± β Sort _: Type ?u.4707SortSort _: Type ?u.4707 _} (hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)hdiff : β β¦t: ?m.4711t i: ?m.4714iβ¦, p: Ξ± β Sort ?u.4707p t: ?m.4711t β p: Ξ± β Sort ?u.4707p (t: ?m.4711t \ f: β β Ξ±f i: ?m.4714i)) :
β β¦n: ?m.4759nβ¦, p: Ξ± β Sort ?u.4707p (f: β β Ξ±f n: ?m.4759n) β p: Ξ± β Sort ?u.4707p (disjointed: {Ξ± : Type ?u.4764} β [inst : GeneralizedBooleanAlgebra Ξ±] β (β β Ξ±) β β β Ξ±disjointed f: β β Ξ±f n: ?m.4759n)
| 0: β0 => id: {Ξ± : Sort ?u.4803} β Ξ± β Ξ±id
| n: βn + 1 => fun h: ?m.4903h => byGoals accomplished! π
Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.4707hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))p (disjointed f (n + 1))suffices H: (k : β) β p (f (n + 1) \ β(partialSups f) k)H : β k: ?m.4964k, p: Ξ± β Sort ?u.4707p (f: β β Ξ±f (n: βn + 1: ?m.49881) \ partialSups: {Ξ± : Type ?u.5024} β [inst : SemilatticeSup Ξ±] β (β β Ξ±) β β βo Ξ±partialSups f: β β Ξ±f k: ?m.4964k)Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.4707hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))H: (k : β) β p (f (n + 1) \ β(partialSups f) k)p (disjointed f (n + 1))Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.4707hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))H(k : β) β p (f (n + 1) \ β(partialSups f) k)
Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.4707hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))p (disjointed f (n + 1))Β·Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.4707hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))H: (k : β) β p (f (n + 1) \ β(partialSups f) k)p (disjointed f (n + 1)) Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.4707hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))H: (k : β) β p (f (n + 1) \ β(partialSups f) k)p (disjointed f (n + 1))Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.4707hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))H(k : β) β p (f (n + 1) \ β(partialSups f) k)exact H: (k : β) β p (f (n + 1) \ β(partialSups f) k)H n: βnGoals accomplished! π
Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.4707hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))p (disjointed f (n + 1))rintro k: βkΞ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.4707hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))k: βHp (f (n + 1) \ β(partialSups f) k)
Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.4707hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))p (disjointed f (n + 1))induction' k: βk with k: βk ih: ?m.5213 kihΞ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.5212hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))H.zerop (f (n + 1) \ β(partialSups f) Nat.zero)Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.5212hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))k: βih: p (f (n + 1) \ β(partialSups f) k)H.succp (f (n + 1) \ β(partialSups f) (Nat.succ k))
Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.4707hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))p (disjointed f (n + 1))Β·Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.5212hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))H.zerop (f (n + 1) \ β(partialSups f) Nat.zero) Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.5212hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))H.zerop (f (n + 1) \ β(partialSups f) Nat.zero)Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.5212hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))k: βih: p (f (n + 1) \ β(partialSups f) k)H.succp (f (n + 1) \ β(partialSups f) (Nat.succ k))exact hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)hdiff h: p (f (n + 1))hGoals accomplished! π
Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.4707hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))p (disjointed f (n + 1))rw [Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.5212hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))k: βih: p (f (n + 1) \ β(partialSups f) k)H.succp (f (n + 1) \ β(partialSups f) (Nat.succ k))partialSups_succ: β {Ξ± : Type ?u.5230} [inst : SemilatticeSup Ξ±] (f : β β Ξ±) (n : β),
β(partialSups f) (n + 1) = β(partialSups f) n β f (n + 1)partialSups_succ,Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.5212hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))k: βih: p (f (n + 1) \ β(partialSups f) k)H.succp (f (n + 1) \ (β(partialSups f) k β f (k + 1))) Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.5212hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))k: βih: p (f (n + 1) \ β(partialSups f) k)H.succp (f (n + 1) \ β(partialSups f) (Nat.succ k))β sdiff_sdiff_left: β {Ξ± : Type ?u.5298} [inst : GeneralizedCoheytingAlgebra Ξ±] {a b c : Ξ±}, (a \ b) \ c = a \ (b β c)sdiff_sdiff_leftΞ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.5212hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))k: βih: p (f (n + 1) \ β(partialSups f) k)H.succp ((f (n + 1) \ β(partialSups f) k) \ f (k + 1))]Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.5212hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))k: βih: p (f (n + 1) \ β(partialSups f) k)H.succp ((f (n + 1) \ β(partialSups f) k) \ f (k + 1))
Ξ±: Type ?u.4692Ξ²: Type ?u.4695instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±p: Ξ± β Sort ?u.4707hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)n: βh: p (f (n + 1))p (disjointed f (n + 1))exact hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)hdiff ih: ?m.5213 kihGoals accomplished! π
#align disjointed_rec disjointedRec: {Ξ± : Type u_1} β
[inst : GeneralizedBooleanAlgebra Ξ±] β
{f : β β Ξ±} β {p : Ξ± β Sort u_2} β (β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)) β β¦n : ββ¦ β p (f n) β p (disjointed f n)disjointedRec

@[simp]
theorem disjointedRec_zero: β {Ξ± : Type u_2} [inst : GeneralizedBooleanAlgebra Ξ±] {f : β β Ξ±} {p : Ξ± β Sort u_1}
(hdiff : β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)) (hβ : p (f 0)), disjointedRec hdiff hβ = hβdisjointedRec_zero {f: β β Ξ±f : β: Typeβ β Ξ±: Type ?u.5787Ξ±} {p: Ξ± β Sort u_1p : Ξ±: Type ?u.5787Ξ± β Sort _: Type ?u.5802SortSort _: Type ?u.5802 _} (hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)hdiff : β β¦t: ?m.5806t i: ?m.5809iβ¦, p: Ξ± β Sort ?u.5802p t: ?m.5806t β p: Ξ± β Sort ?u.5802p (t: ?m.5806t \ f: β β Ξ±f i: ?m.5809i))
(hβ: p (f 0)hβ : p: Ξ± β Sort ?u.5802p (f: β β Ξ±f 0: ?m.58540)) : disjointedRec: {Ξ± : Type ?u.5868} β
[inst : GeneralizedBooleanAlgebra Ξ±] β
{f : β β Ξ±} β
{p : Ξ± β Sort ?u.5867} β (β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)) β β¦n : ββ¦ β p (f n) β p (disjointed f n)disjointedRec hdiff: β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)hdiff hβ: p (f 0)hβ = hβ: p (f 0)hβ :=
rfl: β {Ξ± : Sort ?u.5916} {a : Ξ±}, a = arfl
#align disjointed_rec_zero disjointedRec_zero: β {Ξ± : Type u_2} [inst : GeneralizedBooleanAlgebra Ξ±] {f : β β Ξ±} {p : Ξ± β Sort u_1}
(hdiff : β¦t : Ξ±β¦ β β¦i : ββ¦ β p t β p (t \ f i)) (hβ : p (f 0)), disjointedRec hdiff hβ = hβdisjointedRec_zero

-- TODO: Find a useful statement of `disjointedRec_succ`.
theorem Monotone.disjointed_eq: β {f : β β Ξ±}, Monotone f β β (n : β), disjointed f (n + 1) = f (n + 1) \ f nMonotone.disjointed_eq {f: β β Ξ±f : β: Typeβ β Ξ±: Type ?u.5976Ξ±} (hf: Monotone fhf : Monotone: {Ξ± : Type ?u.5990} β {Ξ² : Type ?u.5989} β [inst : Preorder Ξ±] β [inst : Preorder Ξ²] β (Ξ± β Ξ²) β PropMonotone f: β β Ξ±f) (n: βn : β: Typeβ) :
disjointed: {Ξ± : Type ?u.6516} β [inst : GeneralizedBooleanAlgebra Ξ±] β (β β Ξ±) β β β Ξ±disjointed f: β β Ξ±f (n: βn + 1: ?m.65261) = f: β β Ξ±f (n: βn + 1: ?m.65951) \ f: β β Ξ±f n: βn := byGoals accomplished! π Ξ±: Type u_1Ξ²: Type ?u.5979instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±hf: Monotone fn: βdisjointed f (n + 1) = f (n + 1) \ f nrw [Ξ±: Type u_1Ξ²: Type ?u.5979instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±hf: Monotone fn: βdisjointed f (n + 1) = f (n + 1) \ f ndisjointed_succ: β {Ξ± : Type ?u.6653} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β β Ξ±) (n : β),
disjointed f (n + 1) = f (n + 1) \ β(partialSups f) ndisjointed_succ,Ξ±: Type u_1Ξ²: Type ?u.5979instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±hf: Monotone fn: βf (n + 1) \ β(partialSups f) n = f (n + 1) \ f n Ξ±: Type u_1Ξ²: Type ?u.5979instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±hf: Monotone fn: βdisjointed f (n + 1) = f (n + 1) \ f nhf: Monotone fhf.partialSups_eq: β {Ξ± : Type ?u.6683} [inst : SemilatticeSup Ξ±] {f : β β Ξ±}, Monotone f β β(partialSups f) = fpartialSups_eqΞ±: Type u_1Ξ²: Type ?u.5979instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±hf: Monotone fn: βf (n + 1) \ f n = f (n + 1) \ f n]Goals accomplished! π
#align monotone.disjointed_eq Monotone.disjointed_eq: β {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±] {f : β β Ξ±},
Monotone f β β (n : β), disjointed f (n + 1) = f (n + 1) \ f nMonotone.disjointed_eq

@[simp]
theorem partialSups_disjointed: β {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β β Ξ±), partialSups (disjointed f) = partialSups fpartialSups_disjointed (f: β β Ξ±f : β: Typeβ β Ξ±: Type ?u.6807Ξ±) : partialSups: {Ξ± : Type ?u.6821} β [inst : SemilatticeSup Ξ±] β (β β Ξ±) β β βo Ξ±partialSups (disjointed: {Ξ± : Type ?u.6824} β [inst : GeneralizedBooleanAlgebra Ξ±] β (β β Ξ±) β β β Ξ±disjointed f: β β Ξ±f) = partialSups: {Ξ± : Type ?u.6936} β [inst : SemilatticeSup Ξ±] β (β β Ξ±) β β βo Ξ±partialSups f: β β Ξ±f := byGoals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±partialSups (disjointed f) = partialSups fext n: ?Ξ±nΞ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±n: βh.hβ(partialSups (disjointed f)) n = β(partialSups f) n
Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±partialSups (disjointed f) = partialSups finduction' n: ?Ξ±n with k: βk ih: ?m.7500 kihΞ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±h.h.zeroβ(partialSups (disjointed f)) Nat.zero = β(partialSups f) Nat.zeroΞ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±k: βih: β(partialSups (disjointed f)) k = β(partialSups f) kh.h.succβ(partialSups (disjointed f)) (Nat.succ k) = β(partialSups f) (Nat.succ k)
Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±partialSups (disjointed f) = partialSups fΒ·Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±h.h.zeroβ(partialSups (disjointed f)) Nat.zero = β(partialSups f) Nat.zero Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±h.h.zeroβ(partialSups (disjointed f)) Nat.zero = β(partialSups f) Nat.zeroΞ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±k: βih: β(partialSups (disjointed f)) k = β(partialSups f) kh.h.succβ(partialSups (disjointed f)) (Nat.succ k) = β(partialSups f) (Nat.succ k)rw [Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±h.h.zeroβ(partialSups (disjointed f)) Nat.zero = β(partialSups f) Nat.zeropartialSups_zero: β {Ξ± : Type ?u.7511} [inst : SemilatticeSup Ξ±] (f : β β Ξ±), β(partialSups f) 0 = f 0partialSups_zero,Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±h.h.zerodisjointed f 0 = β(partialSups f) Nat.zero Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±h.h.zeroβ(partialSups (disjointed f)) Nat.zero = β(partialSups f) Nat.zeropartialSups_zero: β {Ξ± : Type ?u.7643} [inst : SemilatticeSup Ξ±] (f : β β Ξ±), β(partialSups f) 0 = f 0partialSups_zero,Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±h.h.zerodisjointed f 0 = f 0 Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±h.h.zeroβ(partialSups (disjointed f)) Nat.zero = β(partialSups f) Nat.zerodisjointed_zero: β {Ξ± : Type ?u.7699} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β β Ξ±), disjointed f 0 = f 0disjointed_zeroΞ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±h.h.zerof 0 = f 0]Goals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±partialSups (disjointed f) = partialSups fΒ·Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±k: βih: β(partialSups (disjointed f)) k = β(partialSups f) kh.h.succβ(partialSups (disjointed f)) (Nat.succ k) = β(partialSups f) (Nat.succ k) Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±k: βih: β(partialSups (disjointed f)) k = β(partialSups f) kh.h.succβ(partialSups (disjointed f)) (Nat.succ k) = β(partialSups f) (Nat.succ k)rw [Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±k: βih: β(partialSups (disjointed f)) k = β(partialSups f) kh.h.succβ(partialSups (disjointed f)) (Nat.succ k) = β(partialSups f) (Nat.succ k)partialSups_succ: β {Ξ± : Type ?u.7730} [inst : SemilatticeSup Ξ±] (f : β β Ξ±) (n : β),
β(partialSups f) (n + 1) = β(partialSups f) n β f (n + 1)partialSups_succ,Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±k: βih: β(partialSups (disjointed f)) k = β(partialSups f) kh.h.succβ(partialSups (disjointed f)) k β disjointed f (k + 1) = β(partialSups f) (Nat.succ k) Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±k: βih: β(partialSups (disjointed f)) k = β(partialSups f) kh.h.succβ(partialSups (disjointed f)) (Nat.succ k) = β(partialSups f) (Nat.succ k)partialSups_succ: β {Ξ± : Type ?u.7788} [inst : SemilatticeSup Ξ±] (f : β β Ξ±) (n : β),
β(partialSups f) (n + 1) = β(partialSups f) n β f (n + 1)partialSups_succ,Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±k: βih: β(partialSups (disjointed f)) k = β(partialSups f) kh.h.succβ(partialSups (disjointed f)) k β disjointed f (k + 1) = β(partialSups f) k β f (k + 1) Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±k: βih: β(partialSups (disjointed f)) k = β(partialSups f) kh.h.succβ(partialSups (disjointed f)) (Nat.succ k) = β(partialSups f) (Nat.succ k)disjointed_succ: β {Ξ± : Type ?u.7855} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β β Ξ±) (n : β),
disjointed f (n + 1) = f (n + 1) \ β(partialSups f) ndisjointed_succ,Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±k: βih: β(partialSups (disjointed f)) k = β(partialSups f) kh.h.succβ(partialSups (disjointed f)) k β f (k + 1) \ β(partialSups f) k = β(partialSups f) k β f (k + 1) Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±k: βih: β(partialSups (disjointed f)) k = β(partialSups f) kh.h.succβ(partialSups (disjointed f)) (Nat.succ k) = β(partialSups f) (Nat.succ k)ih: ?m.7500 kih,Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±k: βih: β(partialSups (disjointed f)) k = β(partialSups f) kh.h.succβ(partialSups f) k β f (k + 1) \ β(partialSups f) k = β(partialSups f) k β f (k + 1) Ξ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±k: βih: β(partialSups (disjointed f)) k = β(partialSups f) kh.h.succβ(partialSups (disjointed f)) (Nat.succ k) = β(partialSups f) (Nat.succ k)sup_sdiff_self_right: β {Ξ± : Type ?u.7880} [inst : GeneralizedCoheytingAlgebra Ξ±] (a b : Ξ±), a β b \ a = a β bsup_sdiff_self_rightΞ±: Type u_1Ξ²: Type ?u.6810instβ: GeneralizedBooleanAlgebra Ξ±f: β β Ξ±k: βih: β(partialSups (disjointed f)) k = β(partialSups f) kh.h.succβ(partialSups f) k β f (k + 1) = β(partialSups f) k β f (k + 1)]Goals accomplished! π
#align partial_sups_disjointed partialSups_disjointed: β {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β β Ξ±), partialSups (disjointed f) = partialSups fpartialSups_disjointed

/-- `disjointed f` is the unique sequence that is pairwise disjoint and has the same partial sups
as `f`. -/
theorem disjointed_unique: β {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±] {f d : β β Ξ±},
Pairwise (Disjoint on d) β partialSups d = partialSups f β d = disjointed fdisjointed_unique {f: β β Ξ±f d: β β Ξ±d : β: Typeβ β Ξ±: Type ?u.7987Ξ±} (hdisj: Pairwise (Disjoint on d)hdisj : Pairwise: {Ξ± : Type ?u.8004} β (Ξ± β Ξ± β Prop) β PropPairwise (Disjoint: {Ξ± : Type ?u.8016} β [inst : PartialOrder Ξ±] β [inst : OrderBot Ξ±] β Ξ± β Ξ± β PropDisjoint on d: β β Ξ±d))
(hsups: partialSups d = partialSups fhsups : partialSups: {Ξ± : Type ?u.8189} β [inst : SemilatticeSup Ξ±] β (β β Ξ±) β β βo Ξ±partialSups d: β β Ξ±d = partialSups: {Ξ± : Type ?u.8288} β [inst : SemilatticeSup Ξ±] β (β β Ξ±) β β βo Ξ±partialSups f: β β Ξ±f) : d: β β Ξ±d = disjointed: {Ξ± : Type ?u.8303} β [inst : GeneralizedBooleanAlgebra Ξ±] β (β β Ξ±) β β β Ξ±disjointed f: β β Ξ±f := byGoals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fd = disjointed fext n: ?Ξ±nΞ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βhd n = disjointed f n
Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fd = disjointed fcases' n: ?Ξ±n with n: βnΞ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fh.zerod Nat.zero = disjointed f Nat.zeroΞ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh.succd (Nat.succ n) = disjointed f (Nat.succ n)
Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fd = disjointed fΒ·Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fh.zerod Nat.zero = disjointed f Nat.zero Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fh.zerod Nat.zero = disjointed f Nat.zeroΞ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh.succd (Nat.succ n) = disjointed f (Nat.succ n)rw [Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fh.zerod Nat.zero = disjointed f Nat.zeroβ partialSups_zero: β {Ξ± : Type ?u.8911} [inst : SemilatticeSup Ξ±] (f : β β Ξ±), β(partialSups f) 0 = f 0partialSups_zero d: β β Ξ±d,Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fh.zeroβ(partialSups d) 0 = disjointed f Nat.zero Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fh.zerod Nat.zero = disjointed f Nat.zerohsups: partialSups d = partialSups fhsups,Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fh.zeroβ(partialSups f) 0 = disjointed f Nat.zero Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fh.zerod Nat.zero = disjointed f Nat.zeropartialSups_zero: β {Ξ± : Type ?u.9016} [inst : SemilatticeSup Ξ±] (f : β β Ξ±), β(partialSups f) 0 = f 0partialSups_zero,Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fh.zerof 0 = disjointed f Nat.zero Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fh.zerod Nat.zero = disjointed f Nat.zerodisjointed_zero: β {Ξ± : Type ?u.9082} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β β Ξ±), disjointed f 0 = f 0disjointed_zeroΞ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fh.zerof 0 = f 0]Goals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fd = disjointed fsuffices h: d (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nh : d: β β Ξ±d n: βn.succ: β β βsucc = partialSups: {Ξ± : Type ?u.9118} β [inst : SemilatticeSup Ξ±] β (β β Ξ±) β β βo Ξ±partialSups d: β β Ξ±d n: βn.succ: β β βsucc \ partialSups: {Ξ± : Type ?u.9164} β [inst : SemilatticeSup Ξ±] β (β β Ξ±) β β βo Ξ±partialSups d: β β Ξ±d n: βnΞ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: d (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nh.succd (Nat.succ n) = disjointed f (Nat.succ n)Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βhd (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) n
Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fd = disjointed fΒ·Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: d (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nh.succd (Nat.succ n) = disjointed f (Nat.succ n) Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: d (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nh.succd (Nat.succ n) = disjointed f (Nat.succ n)Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βhd (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nrw [Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: d (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nh.succd (Nat.succ n) = disjointed f (Nat.succ n)h: d (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nh,Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: d (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nh.succβ(partialSups d) (Nat.succ n) \ β(partialSups d) n = disjointed f (Nat.succ n) Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: d (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nh.succd (Nat.succ n) = disjointed f (Nat.succ n)hsups: partialSups d = partialSups fhsups,Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: d (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nh.succβ(partialSups f) (Nat.succ n) \ β(partialSups f) n = disjointed f (Nat.succ n) Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: d (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nh.succd (Nat.succ n) = disjointed f (Nat.succ n)partialSups_succ: β {Ξ± : Type ?u.9220} [inst : SemilatticeSup Ξ±] (f : β β Ξ±) (n : β),
β(partialSups f) (n + 1) = β(partialSups f) n β f (n + 1)partialSups_succ,Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: d (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nh.succ(β(partialSups f) n β f (n + 1)) \ β(partialSups f) n = disjointed f (Nat.succ n) Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: d (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nh.succd (Nat.succ n) = disjointed f (Nat.succ n)disjointed_succ: β {Ξ± : Type ?u.9279} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β β Ξ±) (n : β),
disjointed f (n + 1) = f (n + 1) \ β(partialSups f) ndisjointed_succ,Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: d (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nh.succ(β(partialSups f) n β f (n + 1)) \ β(partialSups f) n = f (n + 1) \ β(partialSups f) n Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: d (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nh.succd (Nat.succ n) = disjointed f (Nat.succ n)sup_sdiff: β {Ξ± : Type ?u.9301} [inst : GeneralizedCoheytingAlgebra Ξ±] {a b c : Ξ±}, (a β b) \ c = a \ c β b \ csup_sdiff,Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: d (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nh.succβ(partialSups f) n \ β(partialSups f) n β f (n + 1) \ β(partialSups f) n = f (n + 1) \ β(partialSups f) n Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: d (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nh.succd (Nat.succ n) = disjointed f (Nat.succ n)sdiff_self: β {Ξ± : Type ?u.9367} [inst : GeneralizedCoheytingAlgebra Ξ±] {a : Ξ±}, a \ a = β₯sdiff_self,Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: d (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nh.succβ₯ β f (n + 1) \ β(partialSups f) n = f (n + 1) \ β(partialSups f) n Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: d (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nh.succd (Nat.succ n) = disjointed f (Nat.succ n)bot_sup_eq: β {Ξ± : Type ?u.9399} [inst : SemilatticeSup Ξ±] [inst_1 : OrderBot Ξ±] {a : Ξ±}, β₯ β a = abot_sup_eqΞ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: d (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nh.succf (n + 1) \ β(partialSups f) n = f (n + 1) \ β(partialSups f) n]Goals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fd = disjointed frw [Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βhd (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) npartialSups_succ: β {Ξ± : Type ?u.9724} [inst : SemilatticeSup Ξ±] (f : β β Ξ±) (n : β),
β(partialSups f) (n + 1) = β(partialSups f) n β f (n + 1)partialSups_succ,Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βhd (Nat.succ n) = (β(partialSups d) n β d (n + 1)) \ β(partialSups d) n Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βhd (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nsup_sdiff: β {Ξ± : Type ?u.9783} [inst : GeneralizedCoheytingAlgebra Ξ±] {a b c : Ξ±}, (a β b) \ c = a \ c β b \ csup_sdiff,Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βhd (Nat.succ n) = β(partialSups d) n \ β(partialSups d) n β d (n + 1) \ β(partialSups d) n Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βhd (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nsdiff_self: β {Ξ± : Type ?u.9822} [inst : GeneralizedCoheytingAlgebra Ξ±] {a : Ξ±}, a \ a = β₯sdiff_self,Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βhd (Nat.succ n) = β₯ β d (n + 1) \ β(partialSups d) n Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βhd (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nbot_sup_eq: β {Ξ± : Type ?u.9854} [inst : SemilatticeSup Ξ±] [inst_1 : OrderBot Ξ±] {a : Ξ±}, β₯ β a = abot_sup_eq,Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βhd (Nat.succ n) = d (n + 1) \ β(partialSups d) n Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βhd (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) neq_comm: β {Ξ± : Sort ?u.10035} {a b : Ξ±}, a = b β b = aeq_comm,Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βhd (n + 1) \ β(partialSups d) n = d (Nat.succ n) Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βhd (Nat.succ n) = β(partialSups d) (Nat.succ n) \ β(partialSups d) nsdiff_eq_self_iff_disjoint: β {Ξ± : Type ?u.10045} {x y : Ξ±} [inst : GeneralizedBooleanAlgebra Ξ±], x \ y = x β Disjoint y xsdiff_eq_self_iff_disjointΞ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βhDisjoint (β(partialSups d) n) (d (n + 1))]Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βhDisjoint (β(partialSups d) n) (d (n + 1))
Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fd = disjointed fsuffices h: β (m : β), m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))h : β m: ?m.10072m β€ n: βn, Disjoint: {Ξ± : Type ?u.10083} β [inst : PartialOrder Ξ±] β [inst : OrderBot Ξ±] β Ξ± β Ξ± β PropDisjoint (partialSups: {Ξ± : Type ?u.10164} β [inst : SemilatticeSup Ξ±] β (β β Ξ±) β β βo Ξ±partialSups d: β β Ξ±d m: ?m.10072m) (d: β β Ξ±d n: βn.succ: β β βsucc)Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: β (m : β), m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))hDisjoint (β(partialSups d) n) (d (n + 1))Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βhβ (m : β), m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))
Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fd = disjointed fΒ·Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: β (m : β), m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))hDisjoint (β(partialSups d) n) (d (n + 1)) Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βh: β (m : β), m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))hDisjoint (β(partialSups d) n) (d (n + 1))Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn: βhβ (m : β), m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))exact h: β (m : β), m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))h n: βn le_rfl: β {Ξ± : Type ?u.10640} [inst : Preorder Ξ±] {a : Ξ±}, a β€ ale_rflGoals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fd = disjointed frintro m: βm hm: m β€ nhmΞ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn, m: βhm: m β€ nhDisjoint (β(partialSups d) m) (d (Nat.succ n))
Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fd = disjointed finduction' m: βm with m: βm ih: ?m.10785 mihΞ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn, m: βhmβ: m β€ nhm: Nat.zero β€ nh.zeroDisjoint (β(partialSups d) Nat.zero) (d (Nat.succ n))Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn, mβ: βhmβ: mβ β€ nm: βih: m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))hm: Nat.succ m β€ nh.succDisjoint (β(partialSups d) (Nat.succ m)) (d (Nat.succ n))
Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fd = disjointed fΒ·Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn, m: βhmβ: m β€ nhm: Nat.zero β€ nh.zeroDisjoint (β(partialSups d) Nat.zero) (d (Nat.succ n)) Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn, m: βhmβ: m β€ nhm: Nat.zero β€ nh.zeroDisjoint (β(partialSups d) Nat.zero) (d (Nat.succ n))Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn, mβ: βhmβ: mβ β€ nm: βih: m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))hm: Nat.succ m β€ nh.succDisjoint (β(partialSups d) (Nat.succ m)) (d (Nat.succ n))exact hdisj: Pairwise (Disjoint on d)hdisj (Nat.succ_ne_zero: β (n : β), Nat.succ n β  0Nat.succ_ne_zero _: β_).symm: β {Ξ± : Sort ?u.10808} {a b : Ξ±}, a β  b β b β  asymmGoals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fd = disjointed frw [Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn, mβ: βhmβ: mβ β€ nm: βih: m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))hm: Nat.succ m β€ nh.succDisjoint (β(partialSups d) (Nat.succ m)) (d (Nat.succ n))partialSups_succ: β {Ξ± : Type ?u.10821} [inst : SemilatticeSup Ξ±] (f : β β Ξ±) (n : β),
β(partialSups f) (n + 1) = β(partialSups f) n β f (n + 1)partialSups_succ,Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn, mβ: βhmβ: mβ β€ nm: βih: m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))hm: Nat.succ m β€ nh.succDisjoint (β(partialSups d) m β d (m + 1)) (d (Nat.succ n)) Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn, mβ: βhmβ: mβ β€ nm: βih: m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))hm: Nat.succ m β€ nh.succDisjoint (β(partialSups d) (Nat.succ m)) (d (Nat.succ n))disjoint_iff: β {Ξ± : Type ?u.10881} [inst : SemilatticeInf Ξ±] [inst_1 : OrderBot Ξ±] {a b : Ξ±}, Disjoint a b β a β b = β₯disjoint_iff,Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn, mβ: βhmβ: mβ β€ nm: βih: m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))hm: Nat.succ m β€ nh.succ(β(partialSups d) m β d (m + 1)) β d (Nat.succ n) = β₯ Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn, mβ: βhmβ: mβ β€ nm: βih: m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))hm: Nat.succ m β€ nh.succDisjoint (β(partialSups d) (Nat.succ m)) (d (Nat.succ n))inf_sup_right: β {Ξ± : Type ?u.11064} [inst : DistribLattice Ξ±] {x y z : Ξ±}, (y β z) β x = y β x β z β xinf_sup_right,Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn, mβ: βhmβ: mβ β€ nm: βih: m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))hm: Nat.succ m β€ nh.succβ(partialSups d) m β d (Nat.succ n) β d (m + 1) β d (Nat.succ n) = β₯ Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn, mβ: βhmβ: mβ β€ nm: βih: m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))hm: Nat.succ m β€ nh.succDisjoint (β(partialSups d) (Nat.succ m)) (d (Nat.succ n))sup_eq_bot_iff: β {Ξ± : Type ?u.11148} [inst : SemilatticeSup Ξ±] [inst_1 : OrderBot Ξ±] {a b : Ξ±}, a β b = β₯ β a = β₯ β§ b = β₯sup_eq_bot_iff,Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn, mβ: βhmβ: mβ β€ nm: βih: m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))hm: Nat.succ m β€ nh.succβ(partialSups d) m β d (Nat.succ n) = β₯ β§ d (m + 1) β d (Nat.succ n) = β₯ Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn, mβ: βhmβ: mβ β€ nm: βih: m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))hm: Nat.succ m β€ nh.succDisjoint (β(partialSups d) (Nat.succ m)) (d (Nat.succ n))β disjoint_iff: β {Ξ± : Type ?u.11266} [inst : SemilatticeInf Ξ±] [inst_1 : OrderBot Ξ±] {a b : Ξ±}, Disjoint a b β a β b = β₯disjoint_iff,Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn, mβ: βhmβ: mβ β€ nm: βih: m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))hm: Nat.succ m β€ nh.succDisjoint (β(partialSups d) m) (d (Nat.succ n)) β§ d (m + 1) β d (Nat.succ n) = β₯ Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn, mβ: βhmβ: mβ β€ nm: βih: m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))hm: Nat.succ m β€ nh.succDisjoint (β(partialSups d) (Nat.succ m)) (d (Nat.succ n))β disjoint_iff: β {Ξ± : Type ?u.11380} [inst : SemilatticeInf Ξ±] [inst_1 : OrderBot Ξ±] {a b : Ξ±}, Disjoint a b β a β b = β₯disjoint_iffΞ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn, mβ: βhmβ: mβ β€ nm: βih: m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))hm: Nat.succ m β€ nh.succDisjoint (β(partialSups d) m) (d (Nat.succ n)) β§ Disjoint (d (m + 1)) (d (Nat.succ n))]Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fn, mβ: βhmβ: mβ β€ nm: βih: m β€ n β Disjoint (β(partialSups d) m) (d (Nat.succ n))hm: Nat.succ m β€ nh.succDisjoint (β(partialSups d) m) (d (Nat.succ n)) β§ Disjoint (d (m + 1)) (d (Nat.succ n))
Ξ±: Type u_1Ξ²: Type ?u.7990instβ: GeneralizedBooleanAlgebra Ξ±f, d: β β Ξ±hdisj: Pairwise (Disjoint on d)hsups: partialSups d = partialSups fd = disjointed fexact β¨ih: ?m.10785 mih (Nat.le_of_succ_le: β {n m : β}, Nat.succ n β€ m β n β€ mNat.le_of_succ_le hm: Nat.succ m β€ nhm), hdisj: Pairwise (Disjoint on d)hdisj (Nat.lt_succ_of_le: β {n m : β}, n β€ m β n < Nat.succ mNat.lt_succ_of_le hm: Nat.succ m β€ nhm).ne: β {Ξ± : Type ?u.11518} [inst : Preorder Ξ±] {a b : Ξ±}, a < b β a β  bneβ©Goals accomplished! π
#align disjointed_unique disjointed_unique: β {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±] {f d : β β Ξ±},
Pairwise (Disjoint on d) β partialSups d = partialSups f β d = disjointed fdisjointed_unique

end GeneralizedBooleanAlgebra

section CompleteBooleanAlgebra

variable [CompleteBooleanAlgebra: Type ?u.11801 β Type ?u.11801CompleteBooleanAlgebra Ξ±: Type ?u.11582Ξ±]

theorem iSup_disjointed: β {Ξ± : Type u_1} [inst : CompleteBooleanAlgebra Ξ±] (f : β β Ξ±), (β¨ n, disjointed f n) = β¨ n, f niSup_disjointed (f: β β Ξ±f : β: Typeβ β Ξ±: Type ?u.11591Ξ±) : (β¨ n: ?m.11611n, disjointed: {Ξ± : Type ?u.11613} β [inst : GeneralizedBooleanAlgebra Ξ±] β (β β Ξ±) β β β Ξ±disjointed f: β β Ξ±f n: ?m.11611n) = β¨ n: ?m.11695n, f: β β Ξ±f n: ?m.11695n :=
iSup_eq_iSup_of_partialSups_eq_partialSups: β {Ξ± : Type ?u.11702} [inst : CompleteLattice Ξ±] {f g : β β Ξ±}, partialSups f = partialSups g β (β¨ n, f n) = β¨ n, g niSup_eq_iSup_of_partialSups_eq_partialSups (partialSups_disjointed: β {Ξ± : Type ?u.11743} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β β Ξ±), partialSups (disjointed f) = partialSups fpartialSups_disjointed f: β β Ξ±f)
#align supr_disjointed iSup_disjointed: β {Ξ± : Type u_1} [inst : CompleteBooleanAlgebra Ξ±] (f : β β Ξ±), (β¨ n, disjointed f n) = β¨ n, f niSup_disjointed

theorem disjointed_eq_inf_compl: β {Ξ± : Type u_1} [inst : CompleteBooleanAlgebra Ξ±] (f : β β Ξ±) (n : β), disjointed f n = f n β β¨ i, β¨ h, f iαΆdisjointed_eq_inf_compl (f: β β Ξ±f : β: Typeβ β Ξ±: Type ?u.11795Ξ±) (n: βn : β: Typeβ) : disjointed: {Ξ± : Type ?u.11811} β [inst : GeneralizedBooleanAlgebra Ξ±] β (β β Ξ±) β β β Ξ±disjointed f: β β Ξ±f n: βn = f: β β Ξ±f n: βn β β¨ i: ?m.11856i < n: βn, f: β β Ξ±f i: ?m.11856iαΆ := byGoals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±n: βdisjointed f n = f n β β¨ i, β¨ h, f iαΆcases n: βnΞ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±zerodisjointed f Nat.zero = f Nat.zero β β¨ i, β¨ h, f iαΆΞ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±nβ: βsuccdisjointed f (Nat.succ nβ) = f (Nat.succ nβ) β β¨ i, β¨ h, f iαΆ
Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±n: βdisjointed f n = f n β β¨ i, β¨ h, f iαΆΒ·Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±zerodisjointed f Nat.zero = f Nat.zero β β¨ i, β¨ h, f iαΆ Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±zerodisjointed f Nat.zero = f Nat.zero β β¨ i, β¨ h, f iαΆΞ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±nβ: βsuccdisjointed f (Nat.succ nβ) = f (Nat.succ nβ) β β¨ i, β¨ h, f iαΆrw [Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±zerodisjointed f Nat.zero = f Nat.zero β β¨ i, β¨ h, f iαΆdisjointed_zero: β {Ξ± : Type ?u.12055} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β β Ξ±), disjointed f 0 = f 0disjointed_zero,Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±zerof 0 = f Nat.zero β β¨ i, β¨ h, f iαΆ Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±zerodisjointed f Nat.zero = f Nat.zero β β¨ i, β¨ h, f iαΆeq_comm: β {Ξ± : Sort ?u.12103} {a b : Ξ±}, a = b β b = aeq_comm,Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±zero(f Nat.zero β β¨ i, β¨ h, f iαΆ) = f 0 Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±zerodisjointed f Nat.zero = f Nat.zero β β¨ i, β¨ h, f iαΆinf_eq_left: β {Ξ± : Type ?u.12116} [inst : SemilatticeInf Ξ±] {a b : Ξ±}, a β b = a β a β€ binf_eq_leftΞ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±zerof Nat.zero β€ β¨ i, β¨ h, f iαΆ]Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±zerof Nat.zero β€ β¨ i, β¨ h, f iαΆ
Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±zerodisjointed f Nat.zero = f Nat.zero β β¨ i, β¨ h, f iαΆsimp_rw [Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±zerof Nat.zero β€ β¨ i, β¨ h, f iαΆle_iInf_iff: β {Ξ± : Type ?u.12487} {ΞΉ : Sort ?u.12488} [inst : CompleteLattice Ξ±] {f : ΞΉ β Ξ±} {a : Ξ±},
a β€ iInf f β β (i : ΞΉ), a β€ f ile_iInf_iffΞ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±zeroβ (i : β), i < Nat.zero β f Nat.zero β€ f iαΆ]Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±zeroβ (i : β), i < Nat.zero β f Nat.zero β€ f iαΆ
Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±zerodisjointed f Nat.zero = f Nat.zero β β¨ i, β¨ h, f iαΆexact fun i: ?m.12815i hi: ?m.12818hi => (i: ?m.12815i.not_lt_zero: β (n : β), Β¬n < 0not_lt_zero hi: ?m.12818hi).elim: β {C : Sort ?u.12824}, False β CelimGoals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±n: βdisjointed f n = f n β β¨ i, β¨ h, f iαΆsimp_rw [Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±nβ: βsuccdisjointed f (Nat.succ nβ) = f (Nat.succ nβ) β β¨ i, β¨ h, f iαΆdisjointed_succ: β {Ξ± : Type ?u.12944} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β β Ξ±) (n : β),
disjointed f (n + 1) = f (n + 1) \ β(partialSups f) ndisjointed_succ,Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±nβ: βsuccf (nβ + 1) \ β(partialSups f) nβ = f (Nat.succ nβ) β β¨ i, β¨ h, f iαΆ Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±nβ: βsuccdisjointed f (Nat.succ nβ) = f (Nat.succ nβ) β β¨ i, β¨ h, f iαΆpartialSups_eq_biSup: β {Ξ± : Type ?u.13106} [inst : CompleteLattice Ξ±] (f : β β Ξ±) (n : β), β(partialSups f) n = β¨ i, β¨ h, f ipartialSups_eq_biSup,Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±nβ: βsucc(f (nβ + 1) \ β¨ i, β¨ h, f i) = f (Nat.succ nβ) β β¨ i, β¨ h, f iαΆ Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±nβ: βsuccdisjointed f (Nat.succ nβ) = f (Nat.succ nβ) β β¨ i, β¨ h, f iαΆsdiff_eq: β {Ξ± : Type ?u.13306} {x y : Ξ±} [inst : BooleanAlgebra Ξ±], x \ y = x β yαΆsdiff_eq,Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±nβ: βsuccf (nβ + 1) β (β¨ i, β¨ h, f i)αΆ = f (Nat.succ nβ) β β¨ i, β¨ h, f iαΆ Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±nβ: βsuccdisjointed f (Nat.succ nβ) = f (Nat.succ nβ) β β¨ i, β¨ h, f iαΆcompl_iSupΞ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±nβ: βsucc(f (nβ + 1) β β¨ i, β¨ i_1, f iαΆ) = f (Nat.succ nβ) β β¨ i, β¨ h, f iαΆ]Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±nβ: βsucc(f (nβ + 1) β β¨ i, β¨ i_1, f iαΆ) = f (Nat.succ nβ) β β¨ i, β¨ h, f iαΆ
Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±n: βdisjointed f n = f n β β¨ i, β¨ h, f iαΆcongrΞ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±nβ: βsucc.e_a.e_s(fun i => β¨ i_1, f iαΆ) = fun i => β¨ h, f iαΆ
Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±n: βdisjointed f n = f n β β¨ i, β¨ h, f iαΆext i: ?Ξ±iΞ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±nβ, i: βsucc.e_a.e_s.h(β¨ i_1, f iαΆ) = β¨ h, f iαΆ
Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±n: βdisjointed f n = f n β β¨ i, β¨ h, f iαΆrw [Ξ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±nβ, i: βsucc.e_a.e_s.h(β¨ i_1, f iαΆ) = β¨ h, f iαΆNat.lt_succ_iff: β {m n : β}, m < Nat.succ n β m β€ nNat.lt_succ_iffΞ±: Type u_1Ξ²: Type ?u.11798instβ: CompleteBooleanAlgebra Ξ±f: β β Ξ±nβ, i: βsucc.e_a.e_s.h(β¨ i_1, f iαΆ) = β¨ h, f iαΆ]Goals accomplished! π
#align disjointed_eq_inf_compl disjointed_eq_inf_compl: β {Ξ± : Type u_1} [inst : CompleteBooleanAlgebra Ξ±] (f : β β Ξ±) (n : β), disjointed f n = f n β β¨ i, β¨ h, f iαΆdisjointed_eq_inf_compl

end CompleteBooleanAlgebra

/-! ### Set notation variants of lemmas -/

theorem disjointed_subset: β (f : β β Set Ξ±) (n : β), disjointed f n β f ndisjointed_subset (f: β β Set Ξ±f : β: Typeβ β Set: Type ?u.14162 β Type ?u.14162Set Ξ±: Type ?u.14154Ξ±) (n: βn : β: Typeβ) : disjointed: {Ξ± : Type ?u.14178} β [inst : GeneralizedBooleanAlgebra Ξ±] β (β β Ξ±) β β β Ξ±disjointed f: β β Set Ξ±f n: βn β f: β β Set Ξ±f n: βn :=
disjointed_le: β {Ξ± : Type ?u.14221} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β β Ξ±), disjointed f β€ fdisjointed_le f: β β Set Ξ±f n: βn
#align disjointed_subset disjointed_subset: β {Ξ± : Type u_1} (f : β β Set Ξ±) (n : β), disjointed f n β f ndisjointed_subset

theorem iUnion_disjointed: β {Ξ± : Type u_1} {f : β β Set Ξ±}, (Set.iUnion fun n => disjointed f n) = Set.iUnion fun n => f niUnion_disjointed {f: β β Set Ξ±f : β: Typeβ β Set: Type ?u.14255 β Type ?u.14255Set Ξ±: Type ?u.14247Ξ±} : (β n: ?m.14265n, disjointed: {Ξ± : Type ?u.14267} β [inst : GeneralizedBooleanAlgebra Ξ±] β (β β Ξ±) β β β Ξ±disjointed f: β β Set Ξ±f n: ?m.14265n) = β n: ?m.14306n, f: β β Set Ξ±f n: ?m.14306n :=
iSup_disjointed: β {Ξ± : Type ?u.14318} [inst : CompleteBooleanAlgebra Ξ±] (f : β β Ξ±), (β¨ n, disjointed f n) = β¨ n, f niSup_disjointed f: β β Set Ξ±f
#align Union_disjointed iUnion_disjointed: β {Ξ± : Type u_1} {f : β β Set Ξ±}, (Set.iUnion fun n => disjointed f n) = Set.iUnion fun n => f niUnion_disjointed

theorem disjointed_eq_inter_compl: β {Ξ± : Type u_1} (f : β β Set Ξ±) (n : β), disjointed f n = f n β© Set.iInter fun i => Set.iInter fun h => f iαΆdisjointed_eq_inter_compl (f: β β Set Ξ±f : β: Typeβ β Set: Type ?u.14405 β Type ?u.14405Set Ξ±: Type ?u.14397Ξ±) (n: βn : β: Typeβ) : disjointed: {Ξ± : Type ?u.14412} β [inst : GeneralizedBooleanAlgebra Ξ±] β (β β Ξ±) β β β Ξ±disjointed f: β β Set Ξ±f n: βn = f: β β Set Ξ±f n: βn β© β i: ?m.14444i < n: βn, f: β β Set Ξ±f i: ?m.14444iαΆ :=
disjointed_eq_inf_compl: β {Ξ± : Type ?u.14504} [inst : CompleteBooleanAlgebra Ξ±] (f : β β Ξ±) (n : β), disjointed f n = f n β β¨ i, β¨ h, f iαΆdisjointed_eq_inf_compl f: β β Set Ξ±f n: βn
#align disjointed_eq_inter_compl disjointed_eq_inter_compl: β {Ξ± : Type u_1} (f : β β Set Ξ±) (n : β), disjointed f n = f n β© Set.iInter fun i => Set.iInter fun h => f iαΆdisjointed_eq_inter_compl

theorem preimage_find_eq_disjointed: β (s : β β Set Ξ±) (H : β (x : Ξ±), β n, x β s n) [inst : (x : Ξ±) β (n : β) β Decidable (x β s n)] (n : β),
(fun x => Nat.find (_ : β n, x β s n)) β»ΒΉ' {n} = disjointed s npreimage_find_eq_disjointed (s: β β Set Ξ±s : β: Typeβ β Set: Type ?u.14606 β Type ?u.14606Set Ξ±: Type ?u.14598Ξ±) (H: β (x : Ξ±), β n, x β s nH : β x: ?m.14611x, β n: ?m.14617n, x: ?m.14611x β s: β β Set Ξ±s n: ?m.14617n)
[β x: ?m.14643x n: ?m.14646n, Decidable: Prop β TypeDecidable (x: ?m.14643x β s: β β Set Ξ±s n: ?m.14646n)] (n: βn : β: Typeβ) : (fun x: ?m.14676x => Nat.find: {p : β β Prop} β [inst : DecidablePred p] β (β n, p n) β βNat.find (H: β (x : Ξ±), β n, x β s nH x: ?m.14676x)) β»ΒΉ' {n: βn} = disjointed: {Ξ± : Type ?u.14944} β [inst : GeneralizedBooleanAlgebra Ξ±] β (β β Ξ±) β β β Ξ±disjointed s: β β Set Ξ±s n: βn := byGoals accomplished! π
Ξ±: Type u_1Ξ²: Type ?u.14601s: β β Set Ξ±H: β (x : Ξ±), β n, x β s ninstβ: (x : Ξ±) β (n : β) β Decidable (x β s n)n: β(fun x => Nat.find (_ : β n, x β s n)) β»ΒΉ' {n} = disjointed s next x: ?Ξ±xΞ±: Type u_1Ξ²: Type ?u.14601s: β β Set Ξ±H: β (x : Ξ±), β n, x β s ninstβ: (x : Ξ±) β (n : β) β Decidable (x β s n)n: βx: Ξ±hx β (fun x => Nat.find (_ : β n, x β s n)) β»ΒΉ' {n} β x β disjointed s n
Ξ±: Type u_1Ξ²: Type ?u.14601s: β β Set Ξ±H: β (x : Ξ±), β n, x β s ninstβ: (x : Ξ±) β (n : β) β Decidable (x β s n)n: β(fun x => Nat.find (_ : β n, x β s n)) β»ΒΉ' {n} = disjointed s nsimp [Nat.find_eq_iff: β {m : β} {p : β β Prop} [inst : DecidablePred p] (h : β n, p n), Nat.find h = m β p m β§ β (n : β), n < m β Β¬p nNat.find_eq_iff, disjointed_eq_inter_compl: β {Ξ± : Type ?u.15026} (f : β β Set Ξ±) (n : β), disjointed f n = f n β© Set.iInter fun i => Set.iInter fun h => f iαΆdisjointed_eq_inter_compl]Goals accomplished! π
#align preimage_find_eq_disjointed preimage_find_eq_disjointed: β {Ξ± : Type u_1} (s : β β Set Ξ±) (H : β (x : Ξ±), β n, x β s n) [inst : (x : Ξ±) β (n : β) β Decidable (x β s n)] (n : β),
(fun x => Nat.find (_ : β n, x β s n)) β»ΒΉ' {n} = disjointed s npreimage_find_eq_disjointed
```