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 =>
f: ℕ → α
f
0: ?m.53
0
| n + 1 =>
f: ℕ → α
f
(n +
1: ?m.154
1
) \
partialSups: {α : Type ?u.190} → [inst : SemilatticeSup α] → (ℕ → α) → ℕ →o α
partialSups
f: ℕ → α
f
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 :
ℕ: Type
ℕ
) :
disjointed: {α : Type ?u.708} → [inst : GeneralizedBooleanAlgebra α] → (ℕ → α) → ℕ → α
disjointed
f: ℕ → α
f
(n +
1: ?m.718
1
) =
f: ℕ → α
f
(n +
1: ?m.789
1
) \
partialSups: {α : Type ?u.825} → [inst : SemilatticeSup α] → (ℕ → α) → ℕ →o α
partialSups
f: ℕ → α
f
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: ℕ


α: Type u_1

β: Type ?u.1032

inst✝: GeneralizedBooleanAlgebra α


disjointed ≤ id
α: Type u_1

β: Type ?u.1032

inst✝: GeneralizedBooleanAlgebra α

f: ℕ → α


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
α: Type u_1

β: Type ?u.1032

inst✝: GeneralizedBooleanAlgebra α

f: ℕ → α


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


α: 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
α: Type u_1

β: Type ?u.2549

inst✝: GeneralizedBooleanAlgebra α

f: ℕ → α

m, n✝: ℕ

h: m < Nat.succ n✝


succ
α: 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
α: Type u_1

β: Type ?u.2549

inst✝: GeneralizedBooleanAlgebra α

f: ℕ → α

m: ℕ

h: m < Nat.zero


zero
α: Type u_1

β: Type ?u.2549

inst✝: GeneralizedBooleanAlgebra α

f: ℕ → α

m, n✝: ℕ

h: m < Nat.succ n✝


succ

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 =>
id: {α : Sort ?u.4803} → α → α
id
| 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 :
ℕ: Type
ℕ
) :
disjointed: {α : Type ?u.6516} → [inst : GeneralizedBooleanAlgebra α] → (ℕ → α) → ℕ → α
disjointed
f: ℕ → α
f
(n +
1: ?m.6526
1
) =
f: ℕ → α
f
(n +
1: ?m.6595
1
) \
f: ℕ → α
f
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: ℕ → α


α: 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: ℕ → α


α: Type u_1

β: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: ℕ → α


h.h.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: ℕ → α


α: Type u_1

β: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: ℕ → α


h.h.zero
α: Type u_1

β: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: ℕ → α


h.h.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
α: Type u_1

β: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: ℕ → α


h.h.zero
α: Type u_1

β: Type ?u.6810

inst✝: GeneralizedBooleanAlgebra α

f: ℕ → α


h.h.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
α: 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: ℕ → α


α: 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: {α : 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


α: 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


α: Type u_1

β: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: ℕ → α

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f


h.zero
α: Type u_1

β: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: ℕ → α

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: ℕ


h.succ
α: Type u_1

β: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: ℕ → α

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f


α: Type u_1

β: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: ℕ → α

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f


h.zero
α: Type u_1

β: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: ℕ → α

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f


h.zero
α: Type u_1

β: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: ℕ → α

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f

n: ℕ


h.succ
α: Type u_1

β: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: ℕ → α

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f


h.zero
α: Type u_1

β: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: ℕ → α

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f


h.zero
α: Type u_1

β: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: ℕ → α

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f


h.zero
α: Type u_1

β: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: ℕ → α

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f


h.zero
α: Type u_1

β: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: ℕ → α

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f


h.zero
α: Type u_1

β: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: ℕ → α

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f


h.zero
α: Type u_1

β: Type ?u.7990

inst✝: GeneralizedBooleanAlgebra α

f, d: ℕ → α

hdisj: Pairwise (Disjoint on d)

hsups: partialSups d = partialSups f


h.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


α: 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
α: 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


α: 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
α: 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
α: 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
α: 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
α: 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
α: 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
α: 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
α: 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
α: 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
α: 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


α: 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


α: 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


α: 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


α: 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


α: 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
α: 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


α: 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
α: 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
α: 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


α: 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



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 :
ℕ: Type
ℕ
) :
disjointed: {α : Type ?u.11811} → [inst : GeneralizedBooleanAlgebra α] → (ℕ → α) → ℕ → α
disjointed
f: ℕ → α
f
n =
f: ℕ → α
f
n ⊓ ⨅
i: ?m.11856
i
< 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 :
ℕ: Type
ℕ
) :
disjointed: {α : Type ?u.14178} → [inst : GeneralizedBooleanAlgebra α] → (ℕ → α) → ℕ → α
disjointed
f: ℕ → Set α
f
n ⊆
f: ℕ → Set α
f
n :=
disjointed_le: ∀ {α : Type ?u.14221} [inst : GeneralizedBooleanAlgebra α] (f : ℕ → α), disjointed f ≤ f
disjointed_le
f: ℕ → Set α
f
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 :
ℕ: Type
ℕ
) :
disjointed: {α : Type ?u.14412} → [inst : GeneralizedBooleanAlgebra α] → (ℕ → α) → ℕ → α
disjointed
f: ℕ → Set α
f
n =
f: ℕ → Set α
f
n ∩ ⋂
i: ?m.14444
i
< 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 #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 :
ℕ: 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} =
disjointed: {α : Type ?u.14944} → [inst : GeneralizedBooleanAlgebra α] → (ℕ → α) → ℕ → α
disjointed
s: ℕ → Set α
s
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