[GOAL]
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
⊢ disjointed ≤ id
[PROOFSTEP]
rintro f n
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
n : ℕ
⊢ disjointed f n ≤ id f n
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
⊢ disjointed f Nat.zero ≤ id f Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
n✝ : ℕ
⊢ disjointed f (Nat.succ n✝) ≤ id f (Nat.succ n✝)
[PROOFSTEP]
exact sdiff_le
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
⊢ Pairwise (Disjoint on disjointed f)
[PROOFSTEP]
refine' (Symmetric.pairwise_on Disjoint.symm _).2 fun m n h => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
m n : ℕ
h : m < n
⊢ Disjoint (disjointed f m) (disjointed f n)
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
m : ℕ
h : m < Nat.zero
⊢ Disjoint (disjointed f m) (disjointed f Nat.zero)
[PROOFSTEP]
exact (Nat.not_lt_zero _ h).elim
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
m n✝ : ℕ
h : m < Nat.succ n✝
⊢ Disjoint (disjointed f m) (disjointed f (Nat.succ n✝))
[PROOFSTEP]
exact disjoint_sdiff_self_right.mono_left ((disjointed_le f m).trans (le_partialSups_of_le f (Nat.lt_add_one_iff.1 h)))
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)
n : ℕ
h : p (f (n + 1))
⊢ p (disjointed f (n + 1))
[PROOFSTEP]
suffices H : ∀ k, p (f (n + 1) \ partialSups f k)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
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))
[PROOFSTEP]
exact H n
[GOAL]
case H
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)
n : ℕ
h : p (f (n + 1))
⊢ (k : ℕ) → p (f (n + 1) \ ↑(partialSups f) k)
[PROOFSTEP]
rintro k
[GOAL]
case H
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)
n : ℕ
h : p (f (n + 1))
k : ℕ
⊢ p (f (n + 1) \ ↑(partialSups f) k)
[PROOFSTEP]
induction' k with k ih
[GOAL]
case H.zero
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)
n : ℕ
h : p (f (n + 1))
⊢ p (f (n + 1) \ ↑(partialSups f) Nat.zero)
[PROOFSTEP]
exact hdiff h
[GOAL]
case H.succ
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)
n : ℕ
h : p (f (n + 1))
k : ℕ
ih : p (f (n + 1) \ ↑(partialSups f) k)
⊢ p (f (n + 1) \ ↑(partialSups f) (Nat.succ k))
[PROOFSTEP]
rw [partialSups_succ, ← sdiff_sdiff_left]
[GOAL]
case H.succ
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
p : α → Sort u_3
hdiff : ⦃t : α⦄ → ⦃i : ℕ⦄ → p t → p (t \ f i)
n : ℕ
h : p (f (n + 1))
k : ℕ
ih : p (f (n + 1) \ ↑(partialSups f) k)
⊢ p ((f (n + 1) \ ↑(partialSups f) k) \ f (k + 1))
[PROOFSTEP]
exact hdiff ih
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
hf : Monotone f
n : ℕ
⊢ disjointed f (n + 1) = f (n + 1) \ f n
[PROOFSTEP]
rw [disjointed_succ, hf.partialSups_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
⊢ partialSups (disjointed f) = partialSups f
[PROOFSTEP]
ext n
[GOAL]
case h.h
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
n : ℕ
⊢ ↑(partialSups (disjointed f)) n = ↑(partialSups f) n
[PROOFSTEP]
induction' n with k ih
[GOAL]
case h.h.zero
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
⊢ ↑(partialSups (disjointed f)) Nat.zero = ↑(partialSups f) Nat.zero
[PROOFSTEP]
rw [partialSups_zero, partialSups_zero, disjointed_zero]
[GOAL]
case h.h.succ
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
k : ℕ
ih : ↑(partialSups (disjointed f)) k = ↑(partialSups f) k
⊢ ↑(partialSups (disjointed f)) (Nat.succ k) = ↑(partialSups f) (Nat.succ k)
[PROOFSTEP]
rw [partialSups_succ, partialSups_succ, disjointed_succ, ih, sup_sdiff_self_right]
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
⊢ d = disjointed f
[PROOFSTEP]
ext n
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ d n = disjointed f n
[PROOFSTEP]
cases' n with n
[GOAL]
case h.zero
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
⊢ d Nat.zero = disjointed f Nat.zero
[PROOFSTEP]
rw [← partialSups_zero d, hsups, partialSups_zero, disjointed_zero]
[GOAL]
case h.succ
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ d (Nat.succ n) = disjointed f (Nat.succ n)
[PROOFSTEP]
suffices h : d n.succ = partialSups d n.succ \ partialSups d n
[GOAL]
case h.succ
α : Type u_1
β : Type u_2
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
⊢ d (Nat.succ n) = disjointed f (Nat.succ n)
[PROOFSTEP]
rw [h, hsups, partialSups_succ, disjointed_succ, sup_sdiff, sdiff_self, bot_sup_eq]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ d (Nat.succ n) = ↑(partialSups d) (Nat.succ n) \ ↑(partialSups d) n
[PROOFSTEP]
rw [partialSups_succ, sup_sdiff, sdiff_self, bot_sup_eq, eq_comm, sdiff_eq_self_iff_disjoint]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ Disjoint (↑(partialSups d) n) (d (n + 1))
[PROOFSTEP]
suffices h : ∀ m ≤ n, Disjoint (partialSups d m) (d n.succ)
[GOAL]
case h
α : Type u_1
β : Type u_2
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))
⊢ Disjoint (↑(partialSups d) n) (d (n + 1))
[PROOFSTEP]
exact h n le_rfl
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n : ℕ
⊢ ∀ (m : ℕ), m ≤ n → Disjoint (↑(partialSups d) m) (d (Nat.succ n))
[PROOFSTEP]
rintro m hm
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n m : ℕ
hm : m ≤ n
⊢ Disjoint (↑(partialSups d) m) (d (Nat.succ n))
[PROOFSTEP]
induction' m with m ih
[GOAL]
case h.zero
α : Type u_1
β : Type u_2
inst✝ : GeneralizedBooleanAlgebra α
f d : ℕ → α
hdisj : Pairwise (Disjoint on d)
hsups : partialSups d = partialSups f
n m : ℕ
hm✝ : m ≤ n
hm : Nat.zero ≤ n
⊢ Disjoint (↑(partialSups d) Nat.zero) (d (Nat.succ n))
[PROOFSTEP]
exact hdisj (Nat.succ_ne_zero _).symm
[GOAL]
case h.succ
α : Type u_1
β : Type u_2
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
⊢ Disjoint (↑(partialSups d) (Nat.succ m)) (d (Nat.succ n))
[PROOFSTEP]
rw [partialSups_succ, disjoint_iff, inf_sup_right, sup_eq_bot_iff, ← disjoint_iff, ← disjoint_iff]
[GOAL]
case h.succ
α : Type u_1
β : Type u_2
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
⊢ Disjoint (↑(partialSups d) m) (d (Nat.succ n)) ∧ Disjoint (d (m + 1)) (d (Nat.succ n))
[PROOFSTEP]
exact ⟨ih (Nat.le_of_succ_le hm), hdisj (Nat.lt_succ_of_le hm).ne⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
n : ℕ
⊢ disjointed f n = f n ⊓ ⨅ (i : ℕ) (_ : i < n), (f i)ᶜ
[PROOFSTEP]
cases n
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
⊢ disjointed f Nat.zero = f Nat.zero ⊓ ⨅ (i : ℕ) (_ : i < Nat.zero), (f i)ᶜ
[PROOFSTEP]
rw [disjointed_zero, eq_comm, inf_eq_left]
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
⊢ f Nat.zero ≤ ⨅ (i : ℕ) (_ : i < Nat.zero), (f i)ᶜ
[PROOFSTEP]
simp_rw [le_iInf_iff]
[GOAL]
case zero
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
⊢ ∀ (i : ℕ), i < Nat.zero → f Nat.zero ≤ (f i)ᶜ
[PROOFSTEP]
exact fun i hi => (i.not_lt_zero hi).elim
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
n✝ : ℕ
⊢ disjointed f (Nat.succ n✝) = f (Nat.succ n✝) ⊓ ⨅ (i : ℕ) (_ : i < Nat.succ n✝), (f i)ᶜ
[PROOFSTEP]
simp_rw [disjointed_succ, partialSups_eq_biSup, sdiff_eq, compl_iSup]
[GOAL]
case succ
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
n✝ : ℕ
⊢ f (n✝ + 1) ⊓ ⨅ (i : ℕ) (_ : i ≤ n✝), (f i)ᶜ = f (Nat.succ n✝) ⊓ ⨅ (i : ℕ) (_ : i < Nat.succ n✝), (f i)ᶜ
[PROOFSTEP]
congr
[GOAL]
case succ.e_a.e_s
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
n✝ : ℕ
⊢ (fun i => ⨅ (_ : i ≤ n✝), (f i)ᶜ) = fun i => ⨅ (_ : i < Nat.succ n✝), (f i)ᶜ
[PROOFSTEP]
ext i
[GOAL]
case succ.e_a.e_s.h
α : Type u_1
β : Type u_2
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
n✝ i : ℕ
⊢ ⨅ (_ : i ≤ n✝), (f i)ᶜ = ⨅ (_ : i < Nat.succ n✝), (f i)ᶜ
[PROOFSTEP]
rw [Nat.lt_succ_iff]
[GOAL]
α : Type u_1
β : Type u_2
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
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
β : Type u_2
s : ℕ → Set α
H : ∀ (x : α), ∃ n, x ∈ s n
inst✝ : (x : α) → (n : ℕ) → Decidable (x ∈ s n)
n : ℕ
x : α
⊢ x ∈ (fun x => Nat.find (_ : ∃ n, x ∈ s n)) ⁻¹' {n} ↔ x ∈ disjointed s n
[PROOFSTEP]
simp [Nat.find_eq_iff, disjointed_eq_inter_compl]
