case a
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
⊢ f (limsSup F) ≤ liminf f F

case a
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
⊢ liminf f F ≤ f (limsSup F)
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
⊢ f (limsSup F) = liminf f F
apply le_antisymm
case a
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
A : Set.Nonempty {a | ∀ᶠ (n : R) in F, n ≤ a}
⊢ f (limsSup F) ≤ liminf f F
case a
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
⊢ f (limsSup F) ≤ liminf f F
have A : { a : R | ∀ᶠ n : R in F, n ≤ a }.Nonempty := ⟨⊤, by simp⟩
case a
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
A : Set.Nonempty {a | ∀ᶠ (n : R) in F, n ≤ a}
⊢ sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a}) ≤ liminf f F
case a
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
A : Set.Nonempty {a | ∀ᶠ (n : R) in F, n ≤ a}
⊢ f (limsSup F) ≤ liminf f F
rw [limsSup, f_decr.map_sInf_of_continuousAt' f_cont A]
case a.H
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
A : Set.Nonempty {a | ∀ᶠ (n : R) in F, n ≤ a}
⊢ ∀ (c : S), c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a}) → c < liminf f F
case a
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
A : Set.Nonempty {a | ∀ᶠ (n : R) in F, n ≤ a}
⊢ sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a}) ≤ liminf f F
apply le_of_forall_lt
case a.H
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
A : Set.Nonempty {a | ∀ᶠ (n : R) in F, n ≤ a}
c : S
hc : c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a})
⊢ c < liminf f F
case a.H
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
A : Set.Nonempty {a | ∀ᶠ (n : R) in F, n ≤ a}
⊢ ∀ (c : S), c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a}) → c < liminf f F
intro c hc
case a.H
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
A : Set.Nonempty {a | ∀ᶠ (n : R) in F, n ≤ a}
c : S
hc : ∃ a, (∀ᶠ (n : R) in F, n ≤ a) ∧ c < f a
⊢ ∃ a, (∀ᶠ (a_1 : R) in F, a ≤ f a_1) ∧ c < a
case a.H
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
A : Set.Nonempty {a | ∀ᶠ (n : R) in F, n ≤ a}
c : S
hc : c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a})
⊢ c < liminf f F
simp only [liminf, limsInf, lt_sSup_iff, eventually_map, Set.mem_setOf_eq, exists_prop,
  Set.mem_image, exists_exists_and_eq_and] at hc⊢
case a.H.intro.intro
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
A : Set.Nonempty {a | ∀ᶠ (n : R) in F, n ≤ a}
c : S
d : R
hd : ∀ᶠ (n : R) in F, n ≤ d
h'd : c < f d
⊢ ∃ a, (∀ᶠ (a_1 : R) in F, a ≤ f a_1) ∧ c < a
case a.H
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
A : Set.Nonempty {a | ∀ᶠ (n : R) in F, n ≤ a}
c : S
hc : ∃ a, (∀ᶠ (n : R) in F, n ≤ a) ∧ c < f a
⊢ ∃ a, (∀ᶠ (a_1 : R) in F, a ≤ f a_1) ∧ c < a
rcases hc with ⟨d, hd, h'd⟩
case a.H.intro.intro
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
A : Set.Nonempty {a | ∀ᶠ (n : R) in F, n ≤ a}
c : S
d : R
hd : ∀ᶠ (n : R) in F, n ≤ d
h'd : c < f d
⊢ ∀ᶠ (a : R) in F, f d ≤ f a
case a.H.intro.intro
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
A : Set.Nonempty {a | ∀ᶠ (n : R) in F, n ≤ a}
c : S
d : R
hd : ∀ᶠ (n : R) in F, n ≤ d
h'd : c < f d
⊢ ∃ a, (∀ᶠ (a_1 : R) in F, a ≤ f a_1) ∧ c < a
refine' ⟨f d, _, h'd⟩
no goals
case a.H.intro.intro
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
A : Set.Nonempty {a | ∀ᶠ (n : R) in F, n ≤ a}
c : S
d : R
hd : ∀ᶠ (n : R) in F, n ≤ d
h'd : c < f d
⊢ ∀ᶠ (a : R) in F, f d ≤ f a
filter_upwards [hd]with x hx using f_decr hx
no goals
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
⊢ ⊤ ∈ {a | ∀ᶠ (n : R) in F, n ≤ a}
simp
case a.inl
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
h : ⊥ = limsSup F
⊢ liminf f F ≤ f (limsSup F)

case a.inr
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
⊢ liminf f F ≤ f (limsSup F)
case a
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
⊢ liminf f F ≤ f (limsSup F)
rcases eq_or_lt_of_le (bot_le : ⊥ ≤ F.limsSup) with (h | limsSup_ne_bot)
case pos
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
⊢ liminf f F ≤ f (limsSup F)

case neg
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
⊢ liminf f F ≤ f (limsSup F)
case a.inr
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
⊢ liminf f F ≤ f (limsSup F)
by_cases h' : ∃ c, c < F.limsSup ∧ Set.Ioo c F.limsSup = ∅
case neg
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
⊢ False
case neg
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
⊢ liminf f F ≤ f (limsSup F)
by_contra' H
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
⊢ ∃ l, l < limsSup F ∧ Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}

case neg.intro.intro
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
⊢ False
case neg
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
⊢ False
obtain ⟨l, l_lt, h'l⟩ : ∃ l < F.limsSup, Set.Ioc l F.limsSup ⊆ { x : R | f x < F.liminf f }
case neg.intro.intro
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
⊢ False
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
⊢ ∃ l, l < limsSup F ∧ Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}

case neg.intro.intro
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
⊢ False
exact exists_Ioc_subset_of_mem_nhds ((tendsto_order.1 f_cont.tendsto).2 _ H) ⟨⊥, limsSup_ne_bot⟩
case neg.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < limsSup F
⊢ False
case neg.intro.intro
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
⊢ False
obtain ⟨m, l_m, m_lt⟩ : (Set.Ioo l F.limsSup).Nonempty := by
  contrapose! h'
  refine' ⟨l, l_lt, by rwa [Set.not_nonempty_iff_eq_empty] at h'⟩
case neg.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < limsSup F
B : liminf f F ≤ f m
⊢ False
case neg.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < limsSup F
⊢ False
have B : F.liminf f ≤ f m := by
  apply liminf_le_of_frequently_le _
  apply (frequently_lt_of_lt_limsSup (by isBoundedDefault) m_lt).mono
  intro x hx
  exact f_decr hx.le
case neg.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < limsSup F
B : liminf f F ≤ f m
I : f m < liminf f F
⊢ False
case neg.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < limsSup F
B : liminf f F ≤ f m
⊢ False
have I : f m < F.liminf f := h'l ⟨l_m, m_lt.le⟩
no goals
case neg.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < limsSup F
B : liminf f F ≤ f m
I : f m < liminf f F
⊢ False
exact lt_irrefl _ (B.trans_lt I)
case a.inl
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
h : ⊥ = limsSup F
⊢ liminf f F ≤ f ⊥
case a.inl
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
h : ⊥ = limsSup F
⊢ liminf f F ≤ f (limsSup F)
rw [← h]
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
h : ⊥ = limsSup F
⊢ ∃ᶠ (x : R) in F, f x ≤ f ⊥
case a.inl
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
h : ⊥ = limsSup F
⊢ liminf f F ≤ f ⊥
apply liminf_le_of_frequently_le _
case h
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
h : ⊥ = limsSup F
⊢ ∀ (x : R), f x ≤ f ⊥
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
h : ⊥ = limsSup F
⊢ ∃ᶠ (x : R) in F, f x ≤ f ⊥
apply frequently_of_forall
case h
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
h : ⊥ = limsSup F
x : R
⊢ f x ≤ f ⊥
case h
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
h : ⊥ = limsSup F
⊢ ∀ (x : R), f x ≤ f ⊥
intro x
no goals
case h
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
h : ⊥ = limsSup F
x : R
⊢ f x ≤ f ⊥
exact f_decr bot_le
case pos.intro.intro
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
⊢ liminf f F ≤ f (limsSup F)
case pos
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
⊢ liminf f F ≤ f (limsSup F)
rcases h' with ⟨c, c_lt, hc⟩
case pos.intro.intro
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
B : ∃ᶠ (n : R) in F, limsSup F ≤ n
⊢ liminf f F ≤ f (limsSup F)
case pos.intro.intro
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
⊢ liminf f F ≤ f (limsSup F)
have B : ∃ᶠ n in F, F.limsSup ≤ n := by
  apply (frequently_lt_of_lt_limsSup (by isBoundedDefault) c_lt).mono
  intro x hx
  by_contra'
  have : (Set.Ioo c F.limsSup).Nonempty := ⟨x, ⟨hx, this⟩⟩
  simp only [hc, Set.not_nonempty_empty] at this
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
B : ∃ᶠ (n : R) in F, limsSup F ≤ n
⊢ ∃ᶠ (x : R) in F, f x ≤ f (limsSup F)
case pos.intro.intro
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
B : ∃ᶠ (n : R) in F, limsSup F ≤ n
⊢ liminf f F ≤ f (limsSup F)
apply liminf_le_of_frequently_le _
no goals
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
B : ∃ᶠ (n : R) in F, limsSup F ≤ n
⊢ ∃ᶠ (x : R) in F, f x ≤ f (limsSup F)
exact B.mono fun x hx ↦ f_decr hx
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
⊢ ∀ (x : R), c < x → limsSup F ≤ x
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
⊢ ∃ᶠ (n : R) in F, limsSup F ≤ n
apply (frequently_lt_of_lt_limsSup (by isBoundedDefault) c_lt).mono
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
x : R
hx : c < x
⊢ limsSup F ≤ x
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
⊢ ∀ (x : R), c < x → limsSup F ≤ x
intro x hx
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
x : R
hx : c < x
this : x < limsSup F
⊢ False
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
x : R
hx : c < x
⊢ limsSup F ≤ x
by_contra'
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
x : R
hx : c < x
this✝ : x < limsSup F
this : Set.Nonempty (Set.Ioo c (limsSup F))
⊢ False
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
x : R
hx : c < x
this : x < limsSup F
⊢ False
have : (Set.Ioo c F.limsSup).Nonempty := ⟨x, ⟨hx, this⟩⟩
no goals
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
x : R
hx : c < x
this✝ : x < limsSup F
this : Set.Nonempty (Set.Ioo c (limsSup F))
⊢ False
simp only [hc, Set.not_nonempty_empty] at this
no goals
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
⊢ IsCobounded (fun x x_1 => x ≤ x_1) F
isBoundedDefault
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
h' : ¬Set.Nonempty (Set.Ioo l (limsSup F))
⊢ ∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
⊢ Set.Nonempty (Set.Ioo l (limsSup F))
contrapose! h'
no goals
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
h' : ¬Set.Nonempty (Set.Ioo l (limsSup F))
⊢ ∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
refine' ⟨l, l_lt, by rwa [Set.not_nonempty_iff_eq_empty] at h'⟩
no goals
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
h' : ¬Set.Nonempty (Set.Ioo l (limsSup F))
⊢ Set.Ioo l (limsSup F) = ∅
rwa [Set.not_nonempty_iff_eq_empty] at h'
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < limsSup F
⊢ ∃ᶠ (x : R) in F, f x ≤ f m
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < limsSup F
⊢ liminf f F ≤ f m
apply liminf_le_of_frequently_le _
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < limsSup F
⊢ ∀ (x : R), m < x → f x ≤ f m
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < limsSup F
⊢ ∃ᶠ (x : R) in F, f x ≤ f m
apply (frequently_lt_of_lt_limsSup (by isBoundedDefault) m_lt).mono
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < limsSup F
x : R
hx : m < x
⊢ f x ≤ f m
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < limsSup F
⊢ ∀ (x : R), m < x → f x ≤ f m
intro x hx
no goals
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < limsSup F
x : R
hx : m < x
⊢ f x ≤ f m
exact f_decr hx.le
no goals
α : Type u
β : Type v
ι : Type ?u.48095
R : Type u_1
S : Type u_2
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : CompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : CompleteLinearOrder S
inst✝² : TopologicalSpace S
inst✝¹ : OrderTopology S
F : Filter R
inst✝ : NeBot F
f : R → S
f_decr : Antitone f
f_cont : ContinuousAt f (limsSup F)
limsSup_ne_bot : ⊥ < limsSup F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
H : f (limsSup F) < liminf f F
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
m : R
l_m : l < m
m_lt : m < limsSup F
⊢ IsCobounded (fun x x_1 => x ≤ x_1) F
isBoundedDefault