ι : Type u_1
ι' : Type ?u.347734
α : Type u_2
β : Type ?u.347740
γ : Type ?u.347743
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
⊢ ∀ (b : α), ∃ a, b ≤ u a
ι : Type u_1
ι' : Type ?u.347734
α : Type u_2
β : Type ?u.347740
γ : Type ?u.347743
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
⊢ Tendsto u atTop atTop
apply h.tendsto_atTop_atTop
ι : Type u_1
ι' : Type ?u.347734
α : Type u_2
β : Type ?u.347740
γ : Type ?u.347743
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
b : α
⊢ ∃ a, b ≤ u a
ι : Type u_1
ι' : Type ?u.347734
α : Type u_2
β : Type ?u.347740
γ : Type ?u.347743
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
⊢ ∀ (b : α), ∃ a, b ≤ u a
intro b
case intro.intro.intro
ι : Type u_1
ι' : Type ?u.347734
α : Type u_2
β : Type ?u.347740
γ : Type ?u.347743
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
b : α
N : ι
hN : b < u N
⊢ ∃ a, b ≤ u a
ι : Type u_1
ι' : Type ?u.347734
α : Type u_2
β : Type ?u.347740
γ : Type ?u.347743
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
b : α
⊢ ∃ a, b ≤ u a
rcases not_bddAbove_iff.1 H b with ⟨_, ⟨N, rfl⟩, hN⟩
no goals
case intro.intro.intro
ι : Type u_1
ι' : Type ?u.347734
α : Type u_2
β : Type ?u.347740
γ : Type ?u.347743
inst✝¹ : Preorder ι
inst✝ : LinearOrder α
u : ι → α
h : Monotone u
H : ¬BddAbove (range u)
b : α
N : ι
hN : b < u N
⊢ ∃ a, b ≤ u a
exact ⟨N, le_of_lt hN⟩