α : Type u_1
β : Type ?u.106921
γ : Type ?u.106924
ι : Type ?u.106927
inst✝ : CompleteLattice α
u : ℕ → α
⊢ (⨅ (i : ℕ), ⨆ (a : ℕ) (_ : a ∈ Ici i), u a) = ⨅ (n : ℕ), ⨆ (i : ℕ) (_ : i ≥ n), u i
α : Type u_1
β : Type ?u.106921
γ : Type ?u.106924
ι : Type ?u.106927
inst✝ : CompleteLattice α
u : ℕ → α
⊢ (⨅ (i : ℕ) (_ : True), sSup (u '' Ici i)) = ⨅ (n : ℕ), ⨆ (i : ℕ) (_ : i ≥ n), u i
simp only [sSup_image, iInf_const]
no goals
α : Type u_1
β : Type ?u.106921
γ : Type ?u.106924
ι : Type ?u.106927
inst✝ : CompleteLattice α
u : ℕ → α
⊢ (⨅ (i : ℕ), ⨆ (a : ℕ) (_ : a ∈ Ici i), u a) = ⨅ (n : ℕ), ⨆ (i : ℕ) (_ : i ≥ n), u i
rfl