α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.197009
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l (g ∘ f) → IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.197009
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l (g ∘ f) ↔ IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
refine' ⟨_, fun h => h.isBoundedUnder (α := β) hg⟩
case intro
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.197009
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (x : γ) in map (g ∘ f) l, (fun x x_1 => x ≤ x_1) x c
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.197009
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l (g ∘ f) → IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
rintro ⟨c, hc⟩
case intro
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.197009
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((g ∘ f) a) c
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
case intro
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.197009
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (x : γ) in map (g ∘ f) l, (fun x x_1 => x ≤ x_1) x c
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
rw [eventually_map] at hc
case intro.intro
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.197009
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((g ∘ f) a) c
b : β
hb : ∀ (a : β), a ≥ b → c < g a
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
case intro
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.197009
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((g ∘ f) a) c
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
obtain ⟨b, hb⟩ : ∃ b, ∀ a ≥ b, c < g a := eventually_atTop.1 (hg'.eventually_gt_atTop c)
no goals
case intro.intro
α : Type u_3
β : Type u_1
γ : Type u_2
ι : Type ?u.197009
inst✝³ : Nonempty β
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : NoMaxOrder γ
g : β → γ
f : α → β
l : Filter α
hg : Monotone g
hg' : Tendsto g atTop atTop
c : γ
hc : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) ((g ∘ f) a) c
b : β
hb : ∀ (a : β), a ≥ b → c < g a
⊢ IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
exact ⟨b, hc.mono fun x hx => not_lt.1 fun h => (hb _ h.le).not_le hx⟩