case pos
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : f = ⊥
⊢ ∃ c, Tendsto u f (𝓝 c)

case neg
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : ¬f = ⊥
⊢ ∃ c, Tendsto u f (𝓝 c)
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
⊢ ∃ c, Tendsto u f (𝓝 c)
by_cases hbot : f = ⊥
case neg
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : ¬f = ⊥
this : NeBot f
⊢ ∃ c, Tendsto u f (𝓝 c)
case neg
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : ¬f = ⊥
⊢ ∃ c, Tendsto u f (𝓝 c)
haveI : NeBot f := ⟨hbot⟩
case neg
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : ¬f = ⊥
this : NeBot f
⊢ Tendsto u f (𝓝 (limsup u f))
case neg
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : ¬f = ⊥
this : NeBot f
⊢ ∃ c, Tendsto u f (𝓝 c)
refine' ⟨limsup u f, _⟩
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : ¬f = ⊥
this : NeBot f
⊢ limsup u f ≤ liminf u f
case neg
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : ¬f = ⊥
this : NeBot f
⊢ Tendsto u f (𝓝 (limsup u f))
apply tendsto_of_le_liminf_of_limsup_le _ le_rfl h h'
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : ¬f = ⊥
this : NeBot f
hlt : liminf u f < limsup u f
⊢ False
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : ¬f = ⊥
this : NeBot f
⊢ limsup u f ≤ liminf u f
by_contra' hlt
case intro.intro.intro
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : ¬f = ⊥
this : NeBot f
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
⊢ False
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : ¬f = ⊥
this : NeBot f
hlt : liminf u f < limsup u f
⊢ False
obtain ⟨a, ⟨⟨la, au⟩, as⟩⟩ : ∃ a, (f.liminf u < a ∧ a < f.limsup u) ∧ a ∈ s :=
  dense_iff_inter_open.1 hs (Set.Ioo (f.liminf u) (f.limsup u)) isOpen_Ioo
    (Set.nonempty_Ioo.2 hlt)
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : ¬f = ⊥
this : NeBot f
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
b : α
bs : b ∈ s
ab : a < b
bu : b < limsup u f
⊢ False
case intro.intro.intro
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : ¬f = ⊥
this : NeBot f
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
⊢ False
obtain ⟨b, ⟨⟨ab, bu⟩, bs⟩⟩ : ∃ b, (a < b ∧ b < f.limsup u) ∧ b ∈ s :=
  dense_iff_inter_open.1 hs (Set.Ioo a (f.limsup u)) isOpen_Ioo (Set.nonempty_Ioo.2 au)
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : ¬f = ⊥
this : NeBot f
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
b : α
bs : b ∈ s
ab : a < b
bu : b < limsup u f
A : ∃ᶠ (n : β) in f, u n < a
⊢ False
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : ¬f = ⊥
this : NeBot f
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
b : α
bs : b ∈ s
ab : a < b
bu : b < limsup u f
⊢ False
have A : ∃ᶠ n in f, u n < a := frequently_lt_of_liminf_lt (IsBounded.isCobounded_ge h) la
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : ¬f = ⊥
this : NeBot f
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
b : α
bs : b ∈ s
ab : a < b
bu : b < limsup u f
A : ∃ᶠ (n : β) in f, u n < a
B : ∃ᶠ (n : β) in f, b < u n
⊢ False
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : ¬f = ⊥
this : NeBot f
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
b : α
bs : b ∈ s
ab : a < b
bu : b < limsup u f
A : ∃ᶠ (n : β) in f, u n < a
⊢ False
have B : ∃ᶠ n in f, b < u n := frequently_lt_of_lt_limsup (IsBounded.isCobounded_le h') bu
no goals
case intro.intro.intro.intro.intro.intro
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : ¬f = ⊥
this : NeBot f
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
b : α
bs : b ∈ s
ab : a < b
bu : b < limsup u f
A : ∃ᶠ (n : β) in f, u n < a
B : ∃ᶠ (n : β) in f, b < u n
⊢ False
exact H a as b bs ab ⟨A, B⟩
case pos
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : f = ⊥
⊢ ∃ c, Tendsto u ⊥ (𝓝 c)
case pos
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : f = ⊥
⊢ ∃ c, Tendsto u f (𝓝 c)
rw [hbot]
no goals
case pos
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
f : Filter β
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in f, u n < a) ∧ ∃ᶠ (n : β) in f, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) f u) _auto✝
hbot : f = ⊥
⊢ ∃ c, Tendsto u ⊥ (𝓝 c)
exact ⟨sInf ∅, tendsto_bot⟩