α : 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
rintro f n
case zero
α : Type u_1
β : Type ?u.1032
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
⊢ disjointed f Nat.zero ≤ id f Nat.zero

case succ
α : Type u_1
β : Type ?u.1032
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
n✝ : ℕ
⊢ disjointed f (Nat.succ n✝) ≤ id f (Nat.succ n✝)
α : Type u_1
β : Type ?u.1032
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
n : ℕ
⊢ disjointed f n ≤ id f n
cases n
no goals
case zero
α : Type u_1
β : Type ?u.1032
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
⊢ disjointed f Nat.zero ≤ id f Nat.zero
rfl
no goals
case succ
α : Type u_1
β : Type ?u.1032
inst✝ : GeneralizedBooleanAlgebra α
f : ℕ → α
n✝ : ℕ
⊢ disjointed f (Nat.succ n✝) ≤ id f (Nat.succ n✝)
exact sdiff_le