case zero
α : Type u_1
β : Type ?u.11805
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
⊢ disjointed f Nat.zero = f Nat.zero ⊓ ⨅ (i : ℕ) (_ : i < Nat.zero), f iᶜ

case succ
α : Type u_1
β : Type ?u.11805
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
n✝ : ℕ
⊢ disjointed f (Nat.succ n✝) = f (Nat.succ n✝) ⊓ ⨅ (i : ℕ) (_ : i < Nat.succ n✝), f iᶜ
α : Type u_1
β : Type ?u.11805
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
n : ℕ
⊢ disjointed f n = f n ⊓ ⨅ (i : ℕ) (_ : i < n), f iᶜ
cases n
case succ
α : Type u_1
β : Type ?u.11805
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
n✝ : ℕ
⊢ (f (n✝ + 1) ⊓ ⨅ (i : ℕ) (_ : i ≤ n✝), f iᶜ) = f (Nat.succ n✝) ⊓ ⨅ (i : ℕ) (_ : i < Nat.succ n✝), f iᶜ
case succ
α : Type u_1
β : Type ?u.11805
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
n✝ : ℕ
⊢ disjointed f (Nat.succ n✝) = f (Nat.succ n✝) ⊓ ⨅ (i : ℕ) (_ : i < Nat.succ n✝), f iᶜ
simp_rw [disjointed_succ, partialSups_eq_biSup, sdiff_eq, compl_iSup]
case succ.e_a.e_s
α : Type u_1
β : Type ?u.11805
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
n✝ : ℕ
⊢ (fun i => ⨅ (_ : i ≤ n✝), f iᶜ) = fun i => ⨅ (_ : i < Nat.succ n✝), f iᶜ
case succ
α : Type u_1
β : Type ?u.11805
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
n✝ : ℕ
⊢ (f (n✝ + 1) ⊓ ⨅ (i : ℕ) (_ : i ≤ n✝), f iᶜ) = f (Nat.succ n✝) ⊓ ⨅ (i : ℕ) (_ : i < Nat.succ n✝), f iᶜ
congr
case succ.e_a.e_s.h
α : Type u_1
β : Type ?u.11805
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
n✝ i : ℕ
⊢ (⨅ (_ : i ≤ n✝), f iᶜ) = ⨅ (_ : i < Nat.succ n✝), f iᶜ
case succ.e_a.e_s
α : Type u_1
β : Type ?u.11805
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
n✝ : ℕ
⊢ (fun i => ⨅ (_ : i ≤ n✝), f iᶜ) = fun i => ⨅ (_ : i < Nat.succ n✝), f iᶜ
ext i
no goals
case succ.e_a.e_s.h
α : Type u_1
β : Type ?u.11805
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
n✝ i : ℕ
⊢ (⨅ (_ : i ≤ n✝), f iᶜ) = ⨅ (_ : i < Nat.succ n✝), f iᶜ
rw [Nat.lt_succ_iff]
case zero
α : Type u_1
β : Type ?u.11805
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
⊢ f Nat.zero ≤ ⨅ (i : ℕ) (_ : i < Nat.zero), f iᶜ
case zero
α : Type u_1
β : Type ?u.11805
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
⊢ disjointed f Nat.zero = f Nat.zero ⊓ ⨅ (i : ℕ) (_ : i < Nat.zero), f iᶜ
rw [disjointed_zero, eq_comm, inf_eq_left]
case zero
α : Type u_1
β : Type ?u.11805
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
⊢ ∀ (i : ℕ), i < Nat.zero → f Nat.zero ≤ f iᶜ
case zero
α : Type u_1
β : Type ?u.11805
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
⊢ f Nat.zero ≤ ⨅ (i : ℕ) (_ : i < Nat.zero), f iᶜ
simp_rw [le_iInf_iff]
no goals
case zero
α : Type u_1
β : Type ?u.11805
inst✝ : CompleteBooleanAlgebra α
f : ℕ → α
⊢ ∀ (i : ℕ), i < Nat.zero → f Nat.zero ≤ f iᶜ
exact fun i hi => (i.not_lt_zero hi).elim