α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
n : ℕ
this : Set.Iio (n + 1) = Set.Iic n
⊢ ↑(partialSups f) n = ⨆ (i : ↑(Set.Iic n)), f ↑i
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
n : ℕ
⊢ ↑(partialSups f) n = ⨆ (i : ↑(Set.Iic n)), f ↑i
have : Set.Iio (n + 1) = Set.Iic n := Set.ext fun _ => Nat.lt_succ_iff
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
n : ℕ
this : Set.Iio (n + 1) = Set.Iic n
⊢ sSup (f '' Set.Iic n) = sSup (Set.range fun i => f ↑i)
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
n : ℕ
this : Set.Iio (n + 1) = Set.Iic n
⊢ ↑(partialSups f) n = ⨆ (i : ↑(Set.Iic n)), f ↑i
rw [partialSups_eq_sup'_range, Finset.sup'_eq_csSup_image, Finset.coe_range, iSup, this]