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. 
/-
Copyright (c) 2017 Johannes HΓΆlzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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.698
GeneralizedBooleanAlgebra 
Ξ±: 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.53
0
  | 
n: β„•
n + 1 => 
f: β„• β†’ Ξ±
f (
n: β„•
n + 
1: ?m.154
1) \ 
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 0
disjointed_zero (
f: β„• β†’ Ξ±
f : 
β„•: Type
β„• β†’ 
Ξ±: Type ?u.618
Ξ±) : 
disjointed: {Ξ± : Type ?u.632} β†’ [inst : GeneralizedBooleanAlgebra Ξ±] β†’ (β„• β†’ Ξ±) β†’ β„• β†’ Ξ±
disjointed 
f: β„• β†’ Ξ±
f 
0: ?m.639
0 = 
f: β„• β†’ Ξ±
f 
0: ?m.654
0 :=
  
rfl: βˆ€ {Ξ± : Sort ?u.659} {a : Ξ±}, a = a
rfl
#align disjointed_zero 
disjointed_zero: βˆ€ {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β„• β†’ Ξ±), disjointed f 0 = f 0
disjointed_zero

theorem 
disjointed_succ: βˆ€ (f : β„• β†’ Ξ±) (n : β„•), disjointed f (n + 1) = f (n + 1) \ ↑(partialSups f) n
disjointed_succ (
f: β„• β†’ Ξ±
f : 
β„•: Type
β„• β†’ 
Ξ±: Type ?u.692
Ξ±) (
n: β„•
n : 
β„•: Type
β„•) : 
disjointed: {Ξ± : Type ?u.708} β†’ [inst : GeneralizedBooleanAlgebra Ξ±] β†’ (β„• β†’ Ξ±) β†’ β„• β†’ Ξ±
disjointed 
f: β„• β†’ Ξ±
f (
n: β„•
n + 
1: ?m.718
1) = 
f: β„• β†’ Ξ±
f (
n: β„•
n + 
1: ?m.789
1) \ 
partialSups: {Ξ± : Type ?u.825} β†’ [inst : SemilatticeSup Ξ±] β†’ (β„• β†’ Ξ±) β†’ β„• β†’o Ξ±
partialSups 
f: β„• β†’ Ξ±
f 
n: β„•
n :=
  
rfl: βˆ€ {Ξ± : Sort ?u.982} {a : Ξ±}, a = a
rfl
#align disjointed_succ 
disjointed_succ: βˆ€ {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β„• β†’ Ξ±) (n : β„•),
  disjointed f (n + 1) = f (n + 1) \ ↑(partialSups f) n
disjointed_succ

theorem 
disjointed_le_id: βˆ€ {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±], disjointed ≀ id
disjointed_le_id : 
disjointed: {Ξ± : Type ?u.1039} β†’ [inst : GeneralizedBooleanAlgebra Ξ±] β†’ (β„• β†’ Ξ±) β†’ β„• β†’ Ξ±
disjointed ≀ (
id: {Ξ± : Sort ?u.1062} β†’ Ξ± β†’ Ξ±
id : (
β„•: Type
β„• β†’ 
Ξ±: Type ?u.1029
Ξ±) β†’ 
β„•: Type
β„• β†’ 
Ξ±: Type ?u.1029
Ξ±) := 
Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.1032

inst✝: GeneralizedBooleanAlgebra α

disjointed ≀ id
Ξ±: Type u_1

Ξ²: Type ?u.1032

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

n: β„•

disjointed f n ≀ id f n
Ξ±: Type u_1

Ξ²: Type ?u.1032

inst✝: GeneralizedBooleanAlgebra α

disjointed ≀ id
Ξ±: Type u_1

Ξ²: Type ?u.1032

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

zero
disjointed f Nat.zero ≀ id f Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.1032

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

n✝: β„•

succ
disjointed f (Nat.succ n✝) ≀ id f (Nat.succ n✝)
Ξ±: Type u_1

Ξ²: Type ?u.1032

inst✝: GeneralizedBooleanAlgebra α

disjointed ≀ id
Ξ±: Type u_1

Ξ²: Type ?u.1032

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

zero
disjointed f Nat.zero ≀ id f Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.1032

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

zero
disjointed f Nat.zero ≀ id f Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.1032

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

n✝: β„•

succ
disjointed f (Nat.succ n✝) ≀ id f (Nat.succ n✝)
Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.1032

inst✝: GeneralizedBooleanAlgebra α

disjointed ≀ id
Ξ±: Type u_1

Ξ²: Type ?u.1032

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

n✝: β„•

succ
disjointed f (Nat.succ n✝) ≀ id f (Nat.succ n✝)
Ξ±: Type u_1

Ξ²: Type ?u.1032

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

n✝: β„•

succ
disjointed f (Nat.succ n✝) ≀ id f (Nat.succ n✝)
Goals accomplished! πŸ™

#align disjointed_le_id 
disjointed_le_id: βˆ€ {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±], disjointed ≀ id
disjointed_le_id

theorem 
disjointed_le: βˆ€ {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β„• β†’ Ξ±), disjointed f ≀ f
disjointed_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 ≀ id
disjointed_le_id 
f: β„• β†’ Ξ±
f
#align disjointed_le 
disjointed_le: βˆ€ {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β„• β†’ Ξ±), disjointed f ≀ f
disjointed_le

theorem 
disjoint_disjointed: βˆ€ (f : β„• β†’ Ξ±), Pairwise (Disjoint on disjointed f)
disjoint_disjointed (
f: β„• β†’ Ξ±
f : 
β„•: Type
β„• β†’ 
Ξ±: Type ?u.2546
Ξ±) : 
Pairwise: {Ξ± : Type ?u.2559} β†’ (Ξ± β†’ Ξ± β†’ Prop) β†’ Prop
Pairwise (
Disjoint: {Ξ± : Type ?u.2571} β†’ [inst : PartialOrder Ξ±] β†’ [inst : OrderBot Ξ±] β†’ Ξ± β†’ Ξ± β†’ Prop
Disjoint on 
disjointed: {Ξ± : Type ?u.2732} β†’ [inst : GeneralizedBooleanAlgebra Ξ±] β†’ (β„• β†’ Ξ±) β†’ β„• β†’ Ξ±
disjointed 
f: β„• β†’ Ξ±
f) := 
Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.2549

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

Pairwise (Disjoint on disjointed f)
Ξ±: Type u_1

Ξ²: Type ?u.2549

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

m, n: β„•

h: m < n

Disjoint (disjointed f m) (disjointed f n)
Ξ±: Type u_1

Ξ²: Type ?u.2549

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

Pairwise (Disjoint on disjointed f)
Ξ±: Type u_1

Ξ²: Type ?u.2549

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

m: β„•

h: m < Nat.zero

zero
Disjoint (disjointed f m) (disjointed f Nat.zero)
Ξ±: Type u_1

Ξ²: Type ?u.2549

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

m, n✝: β„•

h: m < Nat.succ n✝

succ
Disjoint (disjointed f m) (disjointed f (Nat.succ n✝))
Ξ±: Type u_1

Ξ²: Type ?u.2549

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

Pairwise (Disjoint on disjointed f)
Ξ±: Type u_1

Ξ²: Type ?u.2549

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

m: β„•

h: m < Nat.zero

zero
Disjoint (disjointed f m) (disjointed f Nat.zero)
Ξ±: Type u_1

Ξ²: Type ?u.2549

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

m: β„•

h: m < Nat.zero

zero
Disjoint (disjointed f m) (disjointed f Nat.zero)
Ξ±: Type u_1

Ξ²: Type ?u.2549

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

m, n✝: β„•

h: m < Nat.succ n✝

succ
Disjoint (disjointed f m) (disjointed f (Nat.succ n✝))
Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.2549

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

Pairwise (Disjoint on disjointed f)
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.4707
p : 
Ξ±: Type ?u.4692
Ξ± β†’ 
Sort _: Type ?u.4707
Sort
Sort _: Type ?u.4707
 _} (
hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)
hdiff : βˆ€ ⦃
t: ?m.4711
t 
i: ?m.4714
i⦄, 
p: Ξ± β†’ Sort ?u.4707
p 
t: ?m.4711
t β†’ 
p: Ξ± β†’ Sort ?u.4707
p (
t: ?m.4711
t \ 
f: β„• β†’ Ξ±
f 
i: ?m.4714
i)) :
    βˆ€ ⦃
n: ?m.4759
n⦄, 
p: Ξ± β†’ Sort ?u.4707
p (
f: β„• β†’ Ξ±
f 
n: ?m.4759
n) β†’ 
p: Ξ± β†’ Sort ?u.4707
p (
disjointed: {Ξ± : Type ?u.4764} β†’ [inst : GeneralizedBooleanAlgebra Ξ±] β†’ (β„• β†’ Ξ±) β†’ β„• β†’ Ξ±
disjointed 
f: β„• β†’ Ξ±
f 
n: ?m.4759
n)
  | 
0: β„•
0 => 
id: {Ξ± : Sort ?u.4803} β†’ Ξ± β†’ Ξ±
id
  | 
n: β„•
n + 1 => fun 
h: ?m.4903
h => 
Goals accomplished! πŸ™
Ξ±: Type ?u.4692

Ξ²: Type ?u.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.4707

hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)

n: β„•

h: p (f (n + 1))

p (disjointed f (n + 1))
Ξ±: Type ?u.4692

Ξ²: Type ?u.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.4707

hdiff: ⦃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.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.4707

hdiff: ⦃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.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.4707

hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)

n: β„•

h: p (f (n + 1))

p (disjointed f (n + 1))
Ξ±: Type ?u.4692

Ξ²: Type ?u.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.4707

hdiff: ⦃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.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.4707

hdiff: ⦃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.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.4707

hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)

n: β„•

h: p (f (n + 1))

H
(k : β„•) β†’ p (f (n + 1) \ ↑(partialSups f) k)
Goals accomplished! πŸ™
Ξ±: Type ?u.4692

Ξ²: Type ?u.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.4707

hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)

n: β„•

h: p (f (n + 1))

p (disjointed f (n + 1))
Ξ±: Type ?u.4692

Ξ²: Type ?u.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.4707

hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)

n: β„•

h: p (f (n + 1))

k: β„•

H
p (f (n + 1) \ ↑(partialSups f) k)
Ξ±: Type ?u.4692

Ξ²: Type ?u.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.4707

hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)

n: β„•

h: p (f (n + 1))

p (disjointed f (n + 1))
Ξ±: Type ?u.4692

Ξ²: Type ?u.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.5212

hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)

n: β„•

h: p (f (n + 1))

H.zero
p (f (n + 1) \ ↑(partialSups f) Nat.zero)
Ξ±: Type ?u.4692

Ξ²: Type ?u.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.5212

hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)

n: β„•

h: p (f (n + 1))

k: β„•

ih: p (f (n + 1) \ ↑(partialSups f) k)

H.succ
p (f (n + 1) \ ↑(partialSups f) (Nat.succ k))
Ξ±: Type ?u.4692

Ξ²: Type ?u.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.4707

hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)

n: β„•

h: p (f (n + 1))

p (disjointed f (n + 1))
Ξ±: Type ?u.4692

Ξ²: Type ?u.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.5212

hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)

n: β„•

h: p (f (n + 1))

H.zero
p (f (n + 1) \ ↑(partialSups f) Nat.zero)
Ξ±: Type ?u.4692

Ξ²: Type ?u.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.5212

hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)

n: β„•

h: p (f (n + 1))

H.zero
p (f (n + 1) \ ↑(partialSups f) Nat.zero)
Ξ±: Type ?u.4692

Ξ²: Type ?u.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.5212

hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)

n: β„•

h: p (f (n + 1))

k: β„•

ih: p (f (n + 1) \ ↑(partialSups f) k)

H.succ
p (f (n + 1) \ ↑(partialSups f) (Nat.succ k))
Goals accomplished! πŸ™
Ξ±: Type ?u.4692

Ξ²: Type ?u.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.4707

hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)

n: β„•

h: p (f (n + 1))

p (disjointed f (n + 1))
Ξ±: Type ?u.4692

Ξ²: Type ?u.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.5212

hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)

n: β„•

h: p (f (n + 1))

k: β„•

ih: p (f (n + 1) \ ↑(partialSups f) k)

H.succ
p (f (n + 1) \ ↑(partialSups f) (Nat.succ k))
Ξ±: Type ?u.4692

Ξ²: Type ?u.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.5212

hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)

n: β„•

h: p (f (n + 1))

k: β„•

ih: p (f (n + 1) \ ↑(partialSups f) k)

H.succ
p (f (n + 1) \ (↑(partialSups f) k βŠ” f (k + 1)))
Ξ±: Type ?u.4692

Ξ²: Type ?u.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.5212

hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)

n: β„•

h: p (f (n + 1))

k: β„•

ih: p (f (n + 1) \ ↑(partialSups f) k)

H.succ
p (f (n + 1) \ ↑(partialSups f) (Nat.succ k))
Ξ±: Type ?u.4692

Ξ²: Type ?u.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.5212

hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)

n: β„•

h: p (f (n + 1))

k: β„•

ih: p (f (n + 1) \ ↑(partialSups f) k)

H.succ
p ((f (n + 1) \ ↑(partialSups f) k) \ f (k + 1))
Ξ±: Type ?u.4692

Ξ²: Type ?u.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.5212

hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)

n: β„•

h: p (f (n + 1))

k: β„•

ih: p (f (n + 1) \ ↑(partialSups f) k)

H.succ
p ((f (n + 1) \ ↑(partialSups f) k) \ f (k + 1))
Ξ±: Type ?u.4692

Ξ²: Type ?u.4695

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

p: Ξ± β†’ Sort ?u.4707

hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)

n: β„•

h: p (f (n + 1))

p (disjointed f (n + 1))
Goals 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_1
p : 
Ξ±: Type ?u.5787
Ξ± β†’ 
Sort _: Type ?u.5802
Sort
Sort _: Type ?u.5802
 _} (
hdiff: ⦃t : α⦄ β†’ ⦃i : ℕ⦄ β†’ p t β†’ p (t \ f i)
hdiff : βˆ€ ⦃
t: ?m.5806
t 
i: ?m.5809
i⦄, 
p: Ξ± β†’ Sort ?u.5802
p 
t: ?m.5806
t β†’ 
p: Ξ± β†’ Sort ?u.5802
p (
t: ?m.5806
t \ 
f: β„• β†’ Ξ±
f 
i: ?m.5809
i))
    (
hβ‚€: p (f 0)
hβ‚€ : 
p: Ξ± β†’ Sort ?u.5802
p (
f: β„• β†’ Ξ±
f 
0: ?m.5854
0)) : 
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 = a
rfl
#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 n
Monotone.disjointed_eq {
f: β„• β†’ Ξ±
f : 
β„•: Type
β„• β†’ 
Ξ±: Type ?u.5976
Ξ±} (
hf: Monotone f
hf : 
Monotone: {Ξ± : Type ?u.5990} β†’ {Ξ² : Type ?u.5989} β†’ [inst : Preorder Ξ±] β†’ [inst : Preorder Ξ²] β†’ (Ξ± β†’ Ξ²) β†’ Prop
Monotone 
f: β„• β†’ Ξ±
f) (
n: β„•
n : 
β„•: Type
β„•) :
    
disjointed: {Ξ± : Type ?u.6516} β†’ [inst : GeneralizedBooleanAlgebra Ξ±] β†’ (β„• β†’ Ξ±) β†’ β„• β†’ Ξ±
disjointed 
f: β„• β†’ Ξ±
f (
n: β„•
n + 
1: ?m.6526
1) = 
f: β„• β†’ Ξ±
f (
n: β„•
n + 
1: ?m.6595
1) \ 
f: β„• β†’ Ξ±
f 
n: β„•
n := 
Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.5979

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

hf: Monotone f

n: β„•

disjointed f (n + 1) = f (n + 1) \ f n
Ξ±: Type u_1

Ξ²: Type ?u.5979

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

hf: Monotone f

n: β„•

disjointed f (n + 1) = f (n + 1) \ f n
Ξ±: Type u_1

Ξ²: Type ?u.5979

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

hf: Monotone f

n: β„•

f (n + 1) \ ↑(partialSups f) n = f (n + 1) \ f n
Ξ±: Type u_1

Ξ²: Type ?u.5979

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

hf: Monotone f

n: β„•

disjointed f (n + 1) = f (n + 1) \ f n
Ξ±: Type u_1

Ξ²: Type ?u.5979

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

hf: Monotone f

n: β„•

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 n
Monotone.disjointed_eq

@[simp]
theorem 
partialSups_disjointed: βˆ€ {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β„• β†’ Ξ±), partialSups (disjointed f) = partialSups f
partialSups_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 := 
Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

partialSups (disjointed f) = partialSups f
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

n: β„•

h.h
↑(partialSups (disjointed f)) n = ↑(partialSups f) n
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

partialSups (disjointed f) = partialSups f
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

h.h.zero
↑(partialSups (disjointed f)) Nat.zero = ↑(partialSups f) Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

k: β„•

ih: ↑(partialSups (disjointed f)) k = ↑(partialSups f) k

h.h.succ
↑(partialSups (disjointed f)) (Nat.succ k) = ↑(partialSups f) (Nat.succ k)
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

partialSups (disjointed f) = partialSups f
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

h.h.zero
↑(partialSups (disjointed f)) Nat.zero = ↑(partialSups f) Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

h.h.zero
↑(partialSups (disjointed f)) Nat.zero = ↑(partialSups f) Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

k: β„•

ih: ↑(partialSups (disjointed f)) k = ↑(partialSups f) k

h.h.succ
↑(partialSups (disjointed f)) (Nat.succ k) = ↑(partialSups f) (Nat.succ k)
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

h.h.zero
↑(partialSups (disjointed f)) Nat.zero = ↑(partialSups f) Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

h.h.zero
disjointed f 0 = ↑(partialSups f) Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

h.h.zero
↑(partialSups (disjointed f)) Nat.zero = ↑(partialSups f) Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

h.h.zero
disjointed f 0 = f 0
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

h.h.zero
↑(partialSups (disjointed f)) Nat.zero = ↑(partialSups f) Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

h.h.zero
f 0 = f 0
Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

partialSups (disjointed f) = partialSups f
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

k: β„•

ih: ↑(partialSups (disjointed f)) k = ↑(partialSups f) k

h.h.succ
↑(partialSups (disjointed f)) (Nat.succ k) = ↑(partialSups f) (Nat.succ k)
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

k: β„•

ih: ↑(partialSups (disjointed f)) k = ↑(partialSups f) k

h.h.succ
↑(partialSups (disjointed f)) (Nat.succ k) = ↑(partialSups f) (Nat.succ k)
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

k: β„•

ih: ↑(partialSups (disjointed f)) k = ↑(partialSups f) k

h.h.succ
↑(partialSups (disjointed f)) (Nat.succ k) = ↑(partialSups f) (Nat.succ k)
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

k: β„•

ih: ↑(partialSups (disjointed f)) k = ↑(partialSups f) k

h.h.succ
↑(partialSups (disjointed f)) k βŠ” disjointed f (k + 1) = ↑(partialSups f) (Nat.succ k)
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

k: β„•

ih: ↑(partialSups (disjointed f)) k = ↑(partialSups f) k

h.h.succ
↑(partialSups (disjointed f)) (Nat.succ k) = ↑(partialSups f) (Nat.succ k)
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

k: β„•

ih: ↑(partialSups (disjointed f)) k = ↑(partialSups f) k

h.h.succ
↑(partialSups (disjointed f)) k βŠ” disjointed f (k + 1) = ↑(partialSups f) k βŠ” f (k + 1)
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

k: β„•

ih: ↑(partialSups (disjointed f)) k = ↑(partialSups f) k

h.h.succ
↑(partialSups (disjointed f)) (Nat.succ k) = ↑(partialSups f) (Nat.succ k)
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

k: β„•

ih: ↑(partialSups (disjointed f)) k = ↑(partialSups f) k

h.h.succ
↑(partialSups (disjointed f)) k βŠ” f (k + 1) \ ↑(partialSups f) k = ↑(partialSups f) k βŠ” f (k + 1)
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

k: β„•

ih: ↑(partialSups (disjointed f)) k = ↑(partialSups f) k

h.h.succ
↑(partialSups (disjointed f)) (Nat.succ k) = ↑(partialSups f) (Nat.succ k)
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

k: β„•

ih: ↑(partialSups (disjointed f)) k = ↑(partialSups f) k

h.h.succ
↑(partialSups f) k βŠ” f (k + 1) \ ↑(partialSups f) k = ↑(partialSups f) k βŠ” f (k + 1)
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

k: β„•

ih: ↑(partialSups (disjointed f)) k = ↑(partialSups f) k

h.h.succ
↑(partialSups (disjointed f)) (Nat.succ k) = ↑(partialSups f) (Nat.succ k)
Ξ±: Type u_1

Ξ²: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: β„• β†’ Ξ±

k: β„•

ih: ↑(partialSups (disjointed f)) k = ↑(partialSups f) k

h.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 f
partialSups_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 f
disjointed_unique {
f: β„• β†’ Ξ±
f 
d: β„• β†’ Ξ±
d : 
β„•: Type
β„• β†’ 
Ξ±: Type ?u.7987
Ξ±} (
hdisj: Pairwise (Disjoint on d)
hdisj : 
Pairwise: {Ξ± : Type ?u.8004} β†’ (Ξ± β†’ Ξ± β†’ Prop) β†’ Prop
Pairwise (
Disjoint: {Ξ± : Type ?u.8016} β†’ [inst : PartialOrder Ξ±] β†’ [inst : OrderBot Ξ±] β†’ Ξ± β†’ Ξ± β†’ Prop
Disjoint on 
d: β„• β†’ Ξ±
d))
    (
hsups: partialSups d = partialSups f
hsups : 
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 := 
Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

d = disjointed f
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h
d n = disjointed f n
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

d = disjointed f
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

h.zero
d Nat.zero = disjointed f Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h.succ
d (Nat.succ n) = disjointed f (Nat.succ n)
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

d = disjointed f
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

h.zero
d Nat.zero = disjointed f Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

h.zero
d Nat.zero = disjointed f Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h.succ
d (Nat.succ n) = disjointed f (Nat.succ n)
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

h.zero
d Nat.zero = disjointed f Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

h.zero
↑(partialSups d) 0 = disjointed f Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

h.zero
d Nat.zero = disjointed f Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

h.zero
↑(partialSups f) 0 = disjointed f Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

h.zero
d Nat.zero = disjointed f Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

h.zero
f 0 = disjointed f Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

h.zero
d Nat.zero = disjointed f Nat.zero
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

h.zero
f 0 = f 0
Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

d = disjointed f
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n

h.succ
d (Nat.succ n) = disjointed f (Nat.succ n)
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h
d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

d = disjointed f
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n

h.succ
d (Nat.succ n) = disjointed f (Nat.succ n)
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n

h.succ
d (Nat.succ n) = disjointed f (Nat.succ n)
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h
d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n

h.succ
d (Nat.succ n) = disjointed f (Nat.succ n)
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n

h.succ
↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n = disjointed f (Nat.succ n)
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n

h.succ
d (Nat.succ n) = disjointed f (Nat.succ n)
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n

h.succ
↑(partialSups f) (Nat.succ n) \ ↑(partialSups f) n = disjointed f (Nat.succ n)
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n

h.succ
d (Nat.succ n) = disjointed f (Nat.succ n)
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n

h.succ
(↑(partialSups f) n βŠ” f (n + 1)) \ ↑(partialSups f) n = disjointed f (Nat.succ n)
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n

h.succ
d (Nat.succ n) = disjointed f (Nat.succ n)
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n

h.succ
(↑(partialSups f) n βŠ” f (n + 1)) \ ↑(partialSups f) n = f (n + 1) \ ↑(partialSups f) n
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n

h.succ
d (Nat.succ n) = disjointed f (Nat.succ n)
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n

h.succ
↑(partialSups f) n \ ↑(partialSups f) n βŠ” f (n + 1) \ ↑(partialSups f) n = f (n + 1) \ ↑(partialSups f) n
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n

h.succ
d (Nat.succ n) = disjointed f (Nat.succ n)
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n

h.succ
βŠ₯ βŠ” f (n + 1) \ ↑(partialSups f) n = f (n + 1) \ ↑(partialSups f) n
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n

h.succ
d (Nat.succ n) = disjointed f (Nat.succ n)
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n

h.succ
f (n + 1) \ ↑(partialSups f) n = f (n + 1) \ ↑(partialSups f) n
Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

d = disjointed f
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h
d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h
d (Nat.succ n) = (↑(partialSups d) n βŠ” d (n + 1)) \ ↑(partialSups d) n
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h
d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h
d (Nat.succ n) = ↑(partialSups d) n \ ↑(partialSups d) n βŠ” d (n + 1) \ ↑(partialSups d) n
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h
d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h
d (Nat.succ n) = βŠ₯ βŠ” d (n + 1) \ ↑(partialSups d) n
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h
d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h
d (Nat.succ n) = d (n + 1) \ ↑(partialSups d) n
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h
d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h
d (n + 1) \ ↑(partialSups d) n = d (Nat.succ n)
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h
d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h
Disjoint (↑(partialSups d) n) (d (n + 1))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h
Disjoint (↑(partialSups d) n) (d (n + 1))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

d = disjointed f
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: βˆ€ (m : β„•), m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))

h
Disjoint (↑(partialSups d) n) (d (n + 1))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h
βˆ€ (m : β„•), m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

d = disjointed f
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: βˆ€ (m : β„•), m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))

h
Disjoint (↑(partialSups d) n) (d (n + 1))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h: βˆ€ (m : β„•), m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))

h
Disjoint (↑(partialSups d) n) (d (n + 1))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: β„•

h
βˆ€ (m : β„•), m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))
Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

d = disjointed f
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n, m: β„•

hm: m ≀ n

h
Disjoint (↑(partialSups d) m) (d (Nat.succ n))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

d = disjointed f
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n, m: β„•

hm✝: m ≀ n

hm: Nat.zero ≀ n

h.zero
Disjoint (↑(partialSups d) Nat.zero) (d (Nat.succ n))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n, m✝: β„•

hm✝: m✝ ≀ n

m: β„•

ih: m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))

hm: Nat.succ m ≀ n

h.succ
Disjoint (↑(partialSups d) (Nat.succ m)) (d (Nat.succ n))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

d = disjointed f
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n, m: β„•

hm✝: m ≀ n

hm: Nat.zero ≀ n

h.zero
Disjoint (↑(partialSups d) Nat.zero) (d (Nat.succ n))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n, m: β„•

hm✝: m ≀ n

hm: Nat.zero ≀ n

h.zero
Disjoint (↑(partialSups d) Nat.zero) (d (Nat.succ n))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n, m✝: β„•

hm✝: m✝ ≀ n

m: β„•

ih: m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))

hm: Nat.succ m ≀ n

h.succ
Disjoint (↑(partialSups d) (Nat.succ m)) (d (Nat.succ n))
Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

d = disjointed f
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n, m✝: β„•

hm✝: m✝ ≀ n

m: β„•

ih: m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))

hm: Nat.succ m ≀ n

h.succ
Disjoint (↑(partialSups d) (Nat.succ m)) (d (Nat.succ n))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n, m✝: β„•

hm✝: m✝ ≀ n

m: β„•

ih: m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))

hm: Nat.succ m ≀ n

h.succ
Disjoint (↑(partialSups d) m βŠ” d (m + 1)) (d (Nat.succ n))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n, m✝: β„•

hm✝: m✝ ≀ n

m: β„•

ih: m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))

hm: Nat.succ m ≀ n

h.succ
Disjoint (↑(partialSups d) (Nat.succ m)) (d (Nat.succ n))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n, m✝: β„•

hm✝: m✝ ≀ n

m: β„•

ih: m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))

hm: Nat.succ m ≀ n

h.succ
(↑(partialSups d) m βŠ” d (m + 1)) βŠ“ d (Nat.succ n) = βŠ₯
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n, m✝: β„•

hm✝: m✝ ≀ n

m: β„•

ih: m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))

hm: Nat.succ m ≀ n

h.succ
Disjoint (↑(partialSups d) (Nat.succ m)) (d (Nat.succ n))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n, m✝: β„•

hm✝: m✝ ≀ n

m: β„•

ih: m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))

hm: Nat.succ m ≀ n

h.succ
↑(partialSups d) m βŠ“ d (Nat.succ n) βŠ” d (m + 1) βŠ“ d (Nat.succ n) = βŠ₯
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n, m✝: β„•

hm✝: m✝ ≀ n

m: β„•

ih: m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))

hm: Nat.succ m ≀ n

h.succ
Disjoint (↑(partialSups d) (Nat.succ m)) (d (Nat.succ n))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n, m✝: β„•

hm✝: m✝ ≀ n

m: β„•

ih: m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))

hm: Nat.succ m ≀ n

h.succ
↑(partialSups d) m βŠ“ d (Nat.succ n) = βŠ₯ ∧ d (m + 1) βŠ“ d (Nat.succ n) = βŠ₯
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n, m✝: β„•

hm✝: m✝ ≀ n

m: β„•

ih: m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))

hm: Nat.succ m ≀ n

h.succ
Disjoint (↑(partialSups d) (Nat.succ m)) (d (Nat.succ n))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n, m✝: β„•

hm✝: m✝ ≀ n

m: β„•

ih: m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))

hm: Nat.succ m ≀ n

h.succ
Disjoint (↑(partialSups d) m) (d (Nat.succ n)) ∧ d (m + 1) βŠ“ d (Nat.succ n) = βŠ₯
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n, m✝: β„•

hm✝: m✝ ≀ n

m: β„•

ih: m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))

hm: Nat.succ m ≀ n

h.succ
Disjoint (↑(partialSups d) (Nat.succ m)) (d (Nat.succ n))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n, m✝: β„•

hm✝: m✝ ≀ n

m: β„•

ih: m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))

hm: Nat.succ m ≀ n

h.succ
Disjoint (↑(partialSups d) m) (d (Nat.succ n)) ∧ Disjoint (d (m + 1)) (d (Nat.succ n))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n, m✝: β„•

hm✝: m✝ ≀ n

m: β„•

ih: m ≀ n β†’ Disjoint (↑(partialSups d) m) (d (Nat.succ n))

hm: Nat.succ m ≀ n

h.succ
Disjoint (↑(partialSups d) m) (d (Nat.succ n)) ∧ Disjoint (d (m + 1)) (d (Nat.succ n))
Ξ±: Type u_1

Ξ²: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: β„• β†’ Ξ±

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

d = disjointed f
Goals accomplished! πŸ™

#align disjointed_unique 
disjointed_unique: βˆ€ {Ξ± : Type u_1} [inst : GeneralizedBooleanAlgebra Ξ±] {f d : β„• β†’ Ξ±},
  Pairwise (Disjoint on d) β†’ partialSups d = partialSups f β†’ d = disjointed f
disjointed_unique

end GeneralizedBooleanAlgebra

section CompleteBooleanAlgebra

variable [
CompleteBooleanAlgebra: Type ?u.11801 β†’ Type ?u.11801
CompleteBooleanAlgebra 
Ξ±: Type ?u.11582
Ξ±]

theorem 
iSup_disjointed: βˆ€ {Ξ± : Type u_1} [inst : CompleteBooleanAlgebra Ξ±] (f : β„• β†’ Ξ±), (⨆ n, disjointed f n) = ⨆ n, f n
iSup_disjointed (
f: β„• β†’ Ξ±
f : 
β„•: Type
β„• β†’ 
Ξ±: Type ?u.11591
Ξ±) : (⨆ 
n: ?m.11611
n, 
disjointed: {Ξ± : Type ?u.11613} β†’ [inst : GeneralizedBooleanAlgebra Ξ±] β†’ (β„• β†’ Ξ±) β†’ β„• β†’ Ξ±
disjointed 
f: β„• β†’ Ξ±
f 
n: ?m.11611
n) = ⨆ 
n: ?m.11695
n, 
f: β„• β†’ Ξ±
f 
n: ?m.11695
n :=
  
iSup_eq_iSup_of_partialSups_eq_partialSups: βˆ€ {Ξ± : Type ?u.11702} [inst : CompleteLattice Ξ±] {f g : β„• β†’ Ξ±}, partialSups f = partialSups g β†’ (⨆ n, f n) = ⨆ n, g n
iSup_eq_iSup_of_partialSups_eq_partialSups (
partialSups_disjointed: βˆ€ {Ξ± : Type ?u.11743} [inst : GeneralizedBooleanAlgebra Ξ±] (f : β„• β†’ Ξ±), partialSups (disjointed f) = partialSups f
partialSups_disjointed 
f: β„• β†’ Ξ±
f)
#align supr_disjointed 
iSup_disjointed: βˆ€ {Ξ± : Type u_1} [inst : CompleteBooleanAlgebra Ξ±] (f : β„• β†’ Ξ±), (⨆ n, disjointed f n) = ⨆ n, f n
iSup_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.11856
i < 
n: β„•
n, 
f: β„• β†’ Ξ±
f 
i: ?m.11856
iᢜ := 
Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

n: β„•

disjointed f n = f n βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

zero
disjointed f Nat.zero = f Nat.zero βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

n✝: β„•

succ
disjointed f (Nat.succ n✝) = f (Nat.succ n✝) βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

n: β„•

disjointed f n = f n βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

zero
disjointed f Nat.zero = f Nat.zero βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

zero
disjointed f Nat.zero = f Nat.zero βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

n✝: β„•

succ
disjointed f (Nat.succ n✝) = f (Nat.succ n✝) βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

zero
disjointed f Nat.zero = f Nat.zero βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

zero
f 0 = f Nat.zero βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

zero
disjointed f Nat.zero = f Nat.zero βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

zero
(f Nat.zero βŠ“ β¨… i, β¨… h, f iᢜ) = f 0
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

zero
disjointed f Nat.zero = f Nat.zero βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

zero
f Nat.zero ≀ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

zero
f Nat.zero ≀ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

zero
disjointed f Nat.zero = f Nat.zero βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

zero
f Nat.zero ≀ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

zero
βˆ€ (i : β„•), i < Nat.zero β†’ f Nat.zero ≀ f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

zero
βˆ€ (i : β„•), i < Nat.zero β†’ f Nat.zero ≀ f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

zero
disjointed f Nat.zero = f Nat.zero βŠ“ β¨… i, β¨… h, f iᢜ
Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

n: β„•

disjointed f n = f n βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

n✝: β„•

succ
disjointed f (Nat.succ n✝) = f (Nat.succ n✝) βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

n✝: β„•

succ
f (n✝ + 1) \ ↑(partialSups f) n✝ = f (Nat.succ n✝) βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

n✝: β„•

succ
disjointed f (Nat.succ n✝) = f (Nat.succ n✝) βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

n✝: β„•

succ
(f (n✝ + 1) \ ⨆ i, ⨆ h, f i) = f (Nat.succ n✝) βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

n✝: β„•

succ
disjointed f (Nat.succ n✝) = f (Nat.succ n✝) βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

n✝: β„•

succ
f (n✝ + 1) βŠ“ (⨆ i, ⨆ h, f i)ᢜ = f (Nat.succ n✝) βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

n✝: β„•

succ
disjointed f (Nat.succ n✝) = f (Nat.succ n✝) βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: 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.11798

inst✝: 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.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

n: β„•

disjointed f n = f n βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

n✝: β„•

succ.e_a.e_s
(fun i => β¨… i_1, f iᢜ) = fun i => β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

n: β„•

disjointed f n = f n βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

n✝, i: β„•

succ.e_a.e_s.h
(β¨… i_1, f iᢜ) = β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

n: β„•

disjointed f n = f n βŠ“ β¨… i, β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: CompleteBooleanAlgebra α

f: β„• β†’ Ξ±

n✝, i: β„•

succ.e_a.e_s.h
(β¨… i_1, f iᢜ) = β¨… h, f iᢜ
Ξ±: Type u_1

Ξ²: Type ?u.11798

inst✝: 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 n
disjointed_subset (
f: β„• β†’ Set Ξ±
f : 
β„•: Type
β„• β†’ 
Set: Type ?u.14162 β†’ Type ?u.14162
Set 
Ξ±: 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 ≀ f
disjointed_le 
f: β„• β†’ Set Ξ±
f 
n: β„•
n
#align disjointed_subset 
disjointed_subset: βˆ€ {Ξ± : Type u_1} (f : β„• β†’ Set Ξ±) (n : β„•), disjointed f n βŠ† f n
disjointed_subset

theorem 
iUnion_disjointed: βˆ€ {Ξ± : Type u_1} {f : β„• β†’ Set Ξ±}, (Set.iUnion fun n => disjointed f n) = Set.iUnion fun n => f n
iUnion_disjointed {
f: β„• β†’ Set Ξ±
f : 
β„•: Type
β„• β†’ 
Set: Type ?u.14255 β†’ Type ?u.14255
Set 
Ξ±: Type ?u.14247
Ξ±} : (⋃ 
n: ?m.14265
n, 
disjointed: {Ξ± : Type ?u.14267} β†’ [inst : GeneralizedBooleanAlgebra Ξ±] β†’ (β„• β†’ Ξ±) β†’ β„• β†’ Ξ±
disjointed 
f: β„• β†’ Set Ξ±
f 
n: ?m.14265
n) = ⋃ 
n: ?m.14306
n, 
f: β„• β†’ Set Ξ±
f 
n: ?m.14306
n :=
  
iSup_disjointed: βˆ€ {Ξ± : Type ?u.14318} [inst : CompleteBooleanAlgebra Ξ±] (f : β„• β†’ Ξ±), (⨆ n, disjointed f n) = ⨆ n, f n
iSup_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 n
iUnion_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.14405
Set 
Ξ±: 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.14444
i < 
n: β„•
n, 
f: β„• β†’ Set Ξ±
f 
i: ?m.14444
iᢜ :=
  
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 n
preimage_find_eq_disjointed (
s: β„• β†’ Set Ξ±
s : 
β„•: Type
β„• β†’ 
Set: Type ?u.14606 β†’ Type ?u.14606
Set 
Ξ±: Type ?u.14598
Ξ±) (
H: βˆ€ (x : Ξ±), βˆƒ n, x ∈ s n
H : βˆ€ 
x: ?m.14611
x, βˆƒ 
n: ?m.14617
n, 
x: ?m.14611
x ∈ 
s: β„• β†’ Set Ξ±
s 
n: ?m.14617
n)
    [βˆ€ 
x: ?m.14643
x 
n: ?m.14646
n, 
Decidable: Prop β†’ Type
Decidable (
x: ?m.14643
x ∈ 
s: β„• β†’ Set Ξ±
s 
n: ?m.14646
n)] (
n: β„•
n : 
β„•: Type
β„•) : (fun 
x: ?m.14676
x => 
Nat.find: {p : β„• β†’ Prop} β†’ [inst : DecidablePred p] β†’ (βˆƒ n, p n) β†’ β„•
Nat.find (
H: βˆ€ (x : Ξ±), βˆƒ n, x ∈ s n
H 
x: ?m.14676
x)) ⁻¹' {
n: β„•
n} = 
disjointed: {Ξ± : Type ?u.14944} β†’ [inst : GeneralizedBooleanAlgebra Ξ±] β†’ (β„• β†’ Ξ±) β†’ β„• β†’ Ξ±
disjointed 
s: β„• β†’ Set Ξ±
s 
n: β„•
n := 
Goals accomplished! πŸ™
Ξ±: Type u_1

Ξ²: Type ?u.14601

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 n
Ξ±: Type u_1

Ξ²: Type ?u.14601

s: β„• β†’ Set Ξ±

H: βˆ€ (x : Ξ±), βˆƒ n, x ∈ s n

inst✝: (x : Ξ±) β†’ (n : β„•) β†’ Decidable (x ∈ s n)

n: β„•

x: Ξ±

h
x ∈ (fun x => Nat.find (_ : βˆƒ n, x ∈ s n)) ⁻¹' {n} ↔ x ∈ disjointed s n
Ξ±: Type u_1

Ξ²: Type ?u.14601

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 n
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 n
preimage_find_eq_disjointed