case h.h
α : Type u_1
β : Type ?u.6810
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
n : ℕ
⊢ ↑(partialSups (disjointed f)) n = ↑(partialSups f) n
α : Type u_1
β : Type ?u.6810
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
⊢ partialSups (disjointed f) = partialSups f
ext n
case h.h.zero
α : Type u_1
β : Type ?u.6810
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
⊢ ↑(partialSups (disjointed f)) Nat.zero = ↑(partialSups f) Nat.zero

case h.h.succ
α : Type u_1
β : Type ?u.6810
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
k : ℕ
ih : ↑(partialSups (disjointed f)) k = ↑(partialSups f) k
⊢ ↑(partialSups (disjointed f)) (Nat.succ k) = ↑(partialSups f) (Nat.succ k)
case h.h
α : Type u_1
β : Type ?u.6810
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
n : ℕ
⊢ ↑(partialSups (disjointed f)) n = ↑(partialSups f) n
induction' n with k ih
no goals
case h.h.zero
α : Type u_1
β : Type ?u.6810
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
⊢ ↑(partialSups (disjointed f)) Nat.zero = ↑(partialSups f) Nat.zero
rw [partialSups_zero, partialSups_zero, disjointed_zero]
no goals
case h.h.succ
α : Type u_1
β : Type ?u.6810
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
k : ℕ
ih : ↑(partialSups (disjointed f)) k = ↑(partialSups f) k
⊢ ↑(partialSups (disjointed f)) (Nat.succ k) = ↑(partialSups f) (Nat.succ k)
rw [partialSups_succ, partialSups_succ, disjointed_succ, ih, sup_sdiff_self_right]