case refine'_1
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
h : BddAbove (Set.range f)
n : ℕ
⊢ ↑(partialSups f) n ≤ ⨆ (n : ℕ), f n

case refine'_2
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
h : BddAbove (Set.range f)
⊢ BddAbove (Set.range fun n => ↑(partialSups f) n)
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
h : BddAbove (Set.range f)
⊢ (⨆ (n : ℕ), ↑(partialSups f) n) = ⨆ (n : ℕ), f n
refine' (ciSup_le fun n => _).antisymm (ciSup_mono _ <| le_partialSups f)
case refine'_1
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
h : BddAbove (Set.range f)
n : ℕ
⊢ (⨆ (i : ↑(Set.Iic n)), f ↑i) ≤ ⨆ (n : ℕ), f n
case refine'_1
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
h : BddAbove (Set.range f)
n : ℕ
⊢ ↑(partialSups f) n ≤ ⨆ (n : ℕ), f n
rw [partialSups_eq_ciSup_Iic]
no goals
case refine'_1
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
h : BddAbove (Set.range f)
n : ℕ
⊢ (⨆ (i : ↑(Set.Iic n)), f ↑i) ≤ ⨆ (n : ℕ), f n
exact ciSup_le fun i => le_ciSup h _
no goals
case refine'_2
α : Type u_1
inst✝ : ConditionallyCompleteLattice α
f : ℕ → α
h : BddAbove (Set.range f)
⊢ BddAbove (Set.range fun n => ↑(partialSups f) n)
rwa [bddAbove_range_partialSups]