α : Type ?u.14057
β : Type u_1
γ : Type ?u.14063
ι : Type ?u.14066
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : ℕ → β
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) cofinite f
⊢ BddAbove (range f)
α : Type ?u.14057
β : Type u_1
γ : Type ?u.14063
ι : Type ?u.14066
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : ℕ → β
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) atTop f
⊢ BddAbove (range f)
rw [← Nat.cofinite_eq_atTop] at hf
no goals
α : Type ?u.14057
β : Type u_1
γ : Type ?u.14063
ι : Type ?u.14066
r : α → α → Prop
f✝ g : Filter α
inst✝ : SemilatticeSup β
f : ℕ → β
hf : IsBoundedUnder (fun x x_1 => x ≤ x_1) cofinite f
⊢ BddAbove (range f)
exact hf.bddAbove_range_of_cofinite