case intro
α : Type u_2
β : Type u_1
γ : Type ?u.10574
ι : Type ?u.10577
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (x : β) in map f l, (fun x x_1 => x ≤ x_1) x b
⊢ False
α : Type u_2
β : Type u_1
γ : Type ?u.10574
ι : Type ?u.10577
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
⊢ ¬IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
rintro ⟨b, hb⟩
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.10574
ι : Type ?u.10577
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b
⊢ False
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.10574
ι : Type ?u.10577
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (x : β) in map f l, (fun x x_1 => x ≤ x_1) x b
⊢ False
rw [eventually_map] at hb
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.10574
ι : Type ?u.10577
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b
b' : β
h : b < b'
⊢ False
case intro
α : Type u_2
β : Type u_1
γ : Type ?u.10574
ι : Type ?u.10577
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b
⊢ False
obtain ⟨b', h⟩ := exists_gt b
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.10574
ι : Type ?u.10577
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b
b' : β
h : b < b'
hb' : ∀ᶠ (a : α) in l, b' ≤ f a
⊢ False
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.10574
ι : Type ?u.10577
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b
b' : β
h : b < b'
⊢ False
have hb' := (tendsto_atTop.mp hf) b'
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.10574
ι : Type ?u.10577
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b
b' : β
h : b < b'
hb' : ∀ᶠ (a : α) in l, b' ≤ f a
this : {x | f x ≤ b} ∩ {x | b' ≤ f x} = ∅
⊢ False
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.10574
ι : Type ?u.10577
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b
b' : β
h : b < b'
hb' : ∀ᶠ (a : α) in l, b' ≤ f a
⊢ False
have : { x : α | f x ≤ b } ∩ { x : α | b' ≤ f x } = ∅ :=
  eq_empty_of_subset_empty fun x hx => (not_le_of_lt h) (le_trans hx.2 hx.1)
no goals
case intro.intro
α : Type u_2
β : Type u_1
γ : Type ?u.10574
ι : Type ?u.10577
r : α → α → Prop
f✝ g : Filter α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
f : α → β
l : Filter α
inst✝ : NeBot l
hf : Tendsto f l atTop
b : β
hb : ∀ᶠ (a : α) in l, (fun x x_1 => x ≤ x_1) (f a) b
b' : β
h : b < b'
hb' : ∀ᶠ (a : α) in l, b' ≤ f a
this : {x | f x ≤ b} ∩ {x | b' ≤ f x} = ∅
⊢ False
exact (nonempty_of_mem (hb.and hb')).ne_empty this