[GOAL]
α : 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)
[PROOFSTEP]
rcases f.eq_or_neBot with rfl | hbot
[GOAL]
case inl
α : Type u
β : Type v
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
u : β → α
s : Set α
hs : Dense s
H : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ s → a < b → ¬((∃ᶠ (n : β) in ⊥, u n < a) ∧ ∃ᶠ (n : β) in ⊥, b < u n)
h : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) ⊥ u) _auto✝
h' : autoParam (IsBoundedUnder (fun x x_1 => x ≥ x_1) ⊥ u) _auto✝
⊢ ∃ c, Tendsto u ⊥ (𝓝 c)
[PROOFSTEP]
exact ⟨sInf ∅, tendsto_bot⟩
[GOAL]
case inr
α : 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 : NeBot f
⊢ ∃ c, Tendsto u f (𝓝 c)
[PROOFSTEP]
refine' ⟨limsup u f, _⟩
[GOAL]
case inr
α : 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 : NeBot f
⊢ Tendsto u f (𝓝 (limsup u f))
[PROOFSTEP]
apply tendsto_of_le_liminf_of_limsup_le _ le_rfl h h'
[GOAL]
α : 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 : NeBot f
⊢ limsup u f ≤ liminf u f
[PROOFSTEP]
by_contra' hlt
[GOAL]
α : 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 : NeBot f
hlt : liminf u f < limsup u f
⊢ False
[PROOFSTEP]
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)
[GOAL]
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 : NeBot f
hlt : liminf u f < limsup u f
a : α
as : a ∈ s
la : liminf u f < a
au : a < limsup u f
⊢ False
[PROOFSTEP]
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)
[GOAL]
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 : 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
[PROOFSTEP]
have A : ∃ᶠ n in f, u n < a := frequently_lt_of_liminf_lt (IsBounded.isCobounded_ge h) la
[GOAL]
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 : 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
[PROOFSTEP]
have B : ∃ᶠ n in f, b < u n := frequently_lt_of_lt_limsup (IsBounded.isCobounded_le h') bu
[GOAL]
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 : 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
[PROOFSTEP]
exact H a as b bs ab ⟨A, B⟩
[GOAL]
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f
[PROOFSTEP]
obtain ha | ha := isTop_or_exists_gt (f.limsup u)
[GOAL]
case inl
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : IsTop (limsup u f)
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f
[PROOFSTEP]
exact eventually_of_forall fun _ => ha _
[GOAL]
case inr
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f
[PROOFSTEP]
by_cases H : IsGLB (Set.Ioi (f.limsup u)) (f.limsup u)
[GOAL]
case pos
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : IsGLB (Set.Ioi (limsup u f)) (limsup u f)
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f
[PROOFSTEP]
obtain ⟨u, -, -, hua, hu⟩ := H.exists_seq_antitone_tendsto ha
[GOAL]
case pos.intro.intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u✝ : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u✝) _auto✝
ha : ∃ b, limsup u✝ f < b
H : IsGLB (Set.Ioi (limsup u✝ f)) (limsup u✝ f)
u : ℕ → α
hua : Tendsto u atTop (𝓝 (limsup u✝ f))
hu : ∀ (n : ℕ), u n ∈ Set.Ioi (limsup u✝ f)
⊢ ∀ᶠ (b : β) in f, u✝ b ≤ limsup u✝ f
[PROOFSTEP]
have := fun n => eventually_lt_of_limsup_lt (hu n) hf
[GOAL]
case pos.intro.intro.intro.intro
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u✝ : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u✝) _auto✝
ha : ∃ b, limsup u✝ f < b
H : IsGLB (Set.Ioi (limsup u✝ f)) (limsup u✝ f)
u : ℕ → α
hua : Tendsto u atTop (𝓝 (limsup u✝ f))
hu : ∀ (n : ℕ), u n ∈ Set.Ioi (limsup u✝ f)
this : ∀ (n : ℕ), ∀ᶠ (a : β) in f, u✝ a < u n
⊢ ∀ᶠ (b : β) in f, u✝ b ≤ limsup u✝ f
[PROOFSTEP]
exact (eventually_countable_forall.2 this).mono fun b hb => ge_of_tendsto hua <| eventually_of_forall fun n => (hb _).le
[GOAL]
case neg
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : ¬IsGLB (Set.Ioi (limsup u f)) (limsup u f)
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f
[PROOFSTEP]
obtain ⟨x, hx, xa⟩ : ∃ x, (∀ ⦃b⦄, f.limsup u < b → x ≤ b) ∧ f.limsup u < x :=
  by
  simp only [IsGLB, IsGreatest, lowerBounds, upperBounds, Set.mem_Ioi, Set.mem_setOf_eq, not_and, not_forall, not_le,
    exists_prop] at H
  exact H fun x => le_of_lt
[GOAL]
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : ¬IsGLB (Set.Ioi (limsup u f)) (limsup u f)
⊢ ∃ x, (∀ ⦃b : α⦄, limsup u f < b → x ≤ b) ∧ limsup u f < x
[PROOFSTEP]
simp only [IsGLB, IsGreatest, lowerBounds, upperBounds, Set.mem_Ioi, Set.mem_setOf_eq, not_and, not_forall, not_le,
  exists_prop] at H
[GOAL]
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : (∀ ⦃a : α⦄, limsup u f < a → limsup u f ≤ a) → ∃ x, (∀ ⦃a : α⦄, limsup u f < a → x ≤ a) ∧ limsup u f < x
⊢ ∃ x, (∀ ⦃b : α⦄, limsup u f < b → x ≤ b) ∧ limsup u f < x
[PROOFSTEP]
exact H fun x => le_of_lt
[GOAL]
case neg.intro.intro
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : ¬IsGLB (Set.Ioi (limsup u f)) (limsup u f)
x : α
hx : ∀ ⦃b : α⦄, limsup u f < b → x ≤ b
xa : limsup u f < x
⊢ ∀ᶠ (b : β) in f, u b ≤ limsup u f
[PROOFSTEP]
filter_upwards [eventually_lt_of_limsup_lt xa hf] with y hy
[GOAL]
case h
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : ¬IsGLB (Set.Ioi (limsup u f)) (limsup u f)
x : α
hx : ∀ ⦃b : α⦄, limsup u f < b → x ≤ b
xa : limsup u f < x
y : β
hy : u y < x
⊢ u y ≤ limsup u f
[PROOFSTEP]
contrapose! hy
[GOAL]
case h
α : Type u
β : Type v
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : FirstCountableTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
hf : autoParam (IsBoundedUnder (fun x x_1 => x ≤ x_1) f u) _auto✝
ha : ∃ b, limsup u f < b
H : ¬IsGLB (Set.Ioi (limsup u f)) (limsup u f)
x : α
hx : ∀ ⦃b : α⦄, limsup u f < b → x ≤ b
xa : limsup u f < x
y : β
hy : limsup u f < u y
⊢ x ≤ u y
[PROOFSTEP]
exact hx hy
[GOAL]
α : Type u
β : Type v
inst✝⁴ : CompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : FirstCountableTopology α
inst✝¹ : OrderTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
h : u =ᶠ[f] ⊥
⊢ limsup u f = ⊥
[PROOFSTEP]
rw [limsup_congr h]
[GOAL]
α : Type u
β : Type v
inst✝⁴ : CompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : FirstCountableTopology α
inst✝¹ : OrderTopology α
f : Filter β
inst✝ : CountableInterFilter f
u : β → α
h : u =ᶠ[f] ⊥
⊢ limsup (fun a => ⊥ a) f = ⊥
[PROOFSTEP]
exact limsup_const_bot
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
⊢ f (limsSup F) = liminf f F
[PROOFSTEP]
have cobdd : F.IsCobounded (· ≤ ·) := bdd_below.isCobounded_flip
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
⊢ f (limsSup F) = liminf f F
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
⊢ f (limsSup F) ≤ liminf f F
[PROOFSTEP]
rw [limsSup, f_decr.map_sInf_of_continuousAt' f_cont bdd_above cobdd]
[GOAL]
case a
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
⊢ sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a}) ≤ liminf f F
[PROOFSTEP]
apply le_of_forall_lt
[GOAL]
case a.H
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
⊢ ∀ (c : S), c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a}) → c < liminf f F
[PROOFSTEP]
intro c hc
[GOAL]
case a.H
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
c : S
hc : c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a})
⊢ c < liminf f F
[PROOFSTEP]
simp only [liminf, limsInf, eventually_map] at hc ⊢
[GOAL]
case a.H
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
c : S
hc : c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a})
⊢ c < sSup {a | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}
[PROOFSTEP]
obtain ⟨d, hd, h'd⟩ := exists_lt_of_lt_csSup (bdd_above.recOn fun x hx ↦ ⟨f x, Set.mem_image_of_mem f hx⟩) hc
[GOAL]
case a.H.intro.intro
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
c : S
hc : c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a})
d : S
hd : d ∈ f '' {a | ∀ᶠ (n : R) in F, n ≤ a}
h'd : c < d
⊢ c < sSup {a | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}
[PROOFSTEP]
apply lt_csSup_of_lt ?_ ?_ h'd
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
c : S
hc : c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a})
d : S
hd : d ∈ f '' {a | ∀ᶠ (n : R) in F, n ≤ a}
h'd : c < d
⊢ BddAbove {a | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}
[PROOFSTEP]
exact (Antitone.isBoundedUnder_le_comp f_decr bdd_below).isCoboundedUnder_flip
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
c : S
hc : c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a})
d : S
hd : d ∈ f '' {a | ∀ᶠ (n : R) in F, n ≤ a}
h'd : c < d
⊢ d ∈ {a | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}
[PROOFSTEP]
rcases hd with ⟨e, ⟨he, fe_eq_d⟩⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
c : S
hc : c < sSup (f '' {a | ∀ᶠ (n : R) in F, n ≤ a})
d : S
h'd : c < d
e : R
he : e ∈ {a | ∀ᶠ (n : R) in F, n ≤ a}
fe_eq_d : f e = d
⊢ d ∈ {a | ∀ᶠ (a_1 : R) in F, a ≤ f a_1}
[PROOFSTEP]
filter_upwards [he] with x hx using (fe_eq_d.symm ▸ f_decr hx)
[GOAL]
case a
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
⊢ liminf f F ≤ f (limsSup F)
[PROOFSTEP]
by_cases h' : ∃ c, c < F.limsSup ∧ Set.Ioo c F.limsSup = ∅
[GOAL]
case pos
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
h' : ∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
⊢ liminf f F ≤ f (limsSup F)
[PROOFSTEP]
rcases h' with ⟨c, c_lt, hc⟩
[GOAL]
case pos.intro.intro
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
⊢ liminf f F ≤ f (limsSup F)
[PROOFSTEP]
have B : ∃ᶠ n in F, F.limsSup ≤ n :=
  by
  apply (frequently_lt_of_lt_limsSup cobdd 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
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
⊢ ∃ᶠ (n : R) in F, limsSup F ≤ n
[PROOFSTEP]
apply (frequently_lt_of_lt_limsSup cobdd c_lt).mono
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
⊢ ∀ (x : R), c < x → limsSup F ≤ x
[PROOFSTEP]
intro x hx
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
x : R
hx : c < x
⊢ limsSup F ≤ x
[PROOFSTEP]
by_contra'
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
c : R
c_lt : c < limsSup F
hc : Set.Ioo c (limsSup F) = ∅
x : R
hx : c < x
this : x < limsSup F
⊢ False
[PROOFSTEP]
have : (Set.Ioo c F.limsSup).Nonempty := ⟨x, ⟨hx, this⟩⟩
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) 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
[PROOFSTEP]
simp only [hc, Set.not_nonempty_empty] at this
[GOAL]
case pos.intro.intro
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) 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)
[PROOFSTEP]
apply liminf_le_of_frequently_le _ (bdd_above.isBoundedUnder f_decr)
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) 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)
[PROOFSTEP]
exact (B.mono fun x hx ↦ f_decr hx)
[GOAL]
case neg
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
h' : ¬∃ c, c < limsSup F ∧ Set.Ioo c (limsSup F) = ∅
⊢ liminf f F ≤ f (limsSup F)
[PROOFSTEP]
push_neg at h'
[GOAL]
case neg
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
h' : ∀ (c : R), c < limsSup F → Set.Ioo c (limsSup F) ≠ ∅
⊢ liminf f F ≤ f (limsSup F)
[PROOFSTEP]
by_contra' H
[GOAL]
case neg
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
h' : ∀ (c : R), c < limsSup F → Set.Ioo c (limsSup F) ≠ ∅
H : f (limsSup F) < liminf f F
⊢ False
[PROOFSTEP]
have not_bot : ¬IsBot F.limsSup := fun maybe_bot ↦
  lt_irrefl (F.liminf f) <|
    lt_of_le_of_lt
      (liminf_le_of_frequently_le (frequently_of_forall (fun r ↦ f_decr (maybe_bot r)))
        (bdd_above.isBoundedUnder f_decr))
      H
[GOAL]
case neg
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
h' : ∀ (c : R), c < limsSup F → Set.Ioo c (limsSup F) ≠ ∅
H : f (limsSup F) < liminf f F
not_bot : ¬IsBot (limsSup F)
⊢ False
[PROOFSTEP]
obtain ⟨l, l_lt, h'l⟩ : ∃ l < F.limsSup, Set.Ioc l F.limsSup ⊆ {x : R | f x < F.liminf f}
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
h' : ∀ (c : R), c < limsSup F → Set.Ioo c (limsSup F) ≠ ∅
H : f (limsSup F) < liminf f F
not_bot : ¬IsBot (limsSup F)
⊢ ∃ l, l < limsSup F ∧ Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
[PROOFSTEP]
apply exists_Ioc_subset_of_mem_nhds ((tendsto_order.1 f_cont.tendsto).2 _ H)
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
h' : ∀ (c : R), c < limsSup F → Set.Ioo c (limsSup F) ≠ ∅
H : f (limsSup F) < liminf f F
not_bot : ¬IsBot (limsSup F)
⊢ ∃ l, l < limsSup F
[PROOFSTEP]
simpa [IsBot] using not_bot
[GOAL]
case neg.intro.intro
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
h' : ∀ (c : R), c < limsSup F → Set.Ioo c (limsSup F) ≠ ∅
H : f (limsSup F) < liminf f F
not_bot : ¬IsBot (limsSup F)
l : R
l_lt : l < limsSup F
h'l : Set.Ioc l (limsSup F) ⊆ {x | f x < liminf f F}
⊢ False
[PROOFSTEP]
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' ⟩
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
h' : ∀ (c : R), c < limsSup F → Set.Ioo c (limsSup F) ≠ ∅
H : f (limsSup F) < liminf f F
not_bot : ¬IsBot (limsSup 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))
[PROOFSTEP]
contrapose! h'
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
H : f (limsSup F) < liminf f F
not_bot : ¬IsBot (limsSup 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) = ∅
[PROOFSTEP]
refine' ⟨l, l_lt, by rwa [Set.not_nonempty_iff_eq_empty] at h' ⟩
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
H : f (limsSup F) < liminf f F
not_bot : ¬IsBot (limsSup 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) = ∅
[PROOFSTEP]
rwa [Set.not_nonempty_iff_eq_empty] at h'
[GOAL]
case neg.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
h' : ∀ (c : R), c < limsSup F → Set.Ioo c (limsSup F) ≠ ∅
H : f (limsSup F) < liminf f F
not_bot : ¬IsBot (limsSup 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
[PROOFSTEP]
have B : F.liminf f ≤ f m := by
  apply liminf_le_of_frequently_le _ _
  · apply (frequently_lt_of_lt_limsSup cobdd m_lt).mono
    exact fun x hx ↦ f_decr hx.le
  · exact IsBounded.isBoundedUnder f_decr bdd_above
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
h' : ∀ (c : R), c < limsSup F → Set.Ioo c (limsSup F) ≠ ∅
H : f (limsSup F) < liminf f F
not_bot : ¬IsBot (limsSup 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
[PROOFSTEP]
apply liminf_le_of_frequently_le _ _
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
h' : ∀ (c : R), c < limsSup F → Set.Ioo c (limsSup F) ≠ ∅
H : f (limsSup F) < liminf f F
not_bot : ¬IsBot (limsSup 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
[PROOFSTEP]
apply (frequently_lt_of_lt_limsSup cobdd m_lt).mono
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
h' : ∀ (c : R), c < limsSup F → Set.Ioo c (limsSup F) ≠ ∅
H : f (limsSup F) < liminf f F
not_bot : ¬IsBot (limsSup 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
[PROOFSTEP]
exact fun x hx ↦ f_decr hx.le
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
h' : ∀ (c : R), c < limsSup F → Set.Ioo c (limsSup F) ≠ ∅
H : f (limsSup F) < liminf f F
not_bot : ¬IsBot (limsSup 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
⊢ IsBoundedUnder (fun x x_1 => x ≥ x_1) F f
[PROOFSTEP]
exact IsBounded.isBoundedUnder f_decr bdd_above
[GOAL]
case neg.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
h' : ∀ (c : R), c < limsSup F → Set.Ioo c (limsSup F) ≠ ∅
H : f (limsSup F) < liminf f F
not_bot : ¬IsBot (limsSup 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
[PROOFSTEP]
have I : f m < F.liminf f := h'l ⟨l_m, m_lt.le⟩
[GOAL]
case neg.intro.intro.intro.intro
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
S : Type u_3
F✝ : Filter ι
inst✝⁷ : NeBot F✝
inst✝⁶ : ConditionallyCompleteLinearOrder R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : OrderTopology R
inst✝³ : ConditionallyCompleteLinearOrder 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)
bdd_above : autoParam (IsBounded (fun x x_1 => x ≤ x_1) F) _auto✝
bdd_below : autoParam (IsBounded (fun x x_1 => x ≥ x_1) F) _auto✝
cobdd : IsCobounded (fun x x_1 => x ≤ x_1) F
h' : ∀ (c : R), c < limsSup F → Set.Ioo c (limsSup F) ≠ ∅
H : f (limsSup F) < liminf f F
not_bot : ¬IsBot (limsSup 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
[PROOFSTEP]
exact lt_irrefl _ (B.trans_lt I)
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
x : R
as : ι → R
x_le : ∀ (i : ι), x ≤ as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
⊢ ⨅ (i : ι), as i = x
[PROOFSTEP]
refine' iInf_eq_of_forall_ge_of_forall_gt_exists_lt (fun i ↦ x_le i) _
[GOAL]
α : Type u
β : Type v
ι : Type u_1
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
x : R
as : ι → R
x_le : ∀ (i : ι), x ≤ as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
⊢ ∀ (w : R), x < w → ∃ i, as i < w
[PROOFSTEP]
apply fun w x_lt_w ↦ ‹Filter.NeBot F›.nonempty_of_mem (eventually_lt_of_tendsto_lt x_lt_w as_lim)
[GOAL]
α : Type u
β : Type v
ι✝ : Type u_1
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_3
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
⊢ ⋃ (i : ι), Ici (as i) = Ioi x
[PROOFSTEP]
have obs : x ∉ range as := by
  intro maybe_x_is
  rcases mem_range.mp maybe_x_is with ⟨i, hi⟩
  simpa only [hi, lt_self_iff_false] using x_lt i
[GOAL]
α : Type u
β : Type v
ι✝ : Type u_1
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_3
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
⊢ ¬x ∈ range as
[PROOFSTEP]
intro maybe_x_is
[GOAL]
α : Type u
β : Type v
ι✝ : Type u_1
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_3
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
maybe_x_is : x ∈ range as
⊢ False
[PROOFSTEP]
rcases mem_range.mp maybe_x_is with ⟨i, hi⟩
[GOAL]
case intro
α : Type u
β : Type v
ι✝ : Type u_1
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_3
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
maybe_x_is : x ∈ range as
i : ι
hi : as i = x
⊢ False
[PROOFSTEP]
simpa only [hi, lt_self_iff_false] using x_lt i
[GOAL]
α : Type u
β : Type v
ι✝ : Type u_1
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_3
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
obs : ¬x ∈ range as
⊢ ⋃ (i : ι), Ici (as i) = Ioi x
[PROOFSTEP]
have := iInf_eq_of_forall_le_of_tendsto (fun i ↦ (x_lt i).le) as_lim
[GOAL]
α : Type u
β : Type v
ι✝ : Type u_1
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_3
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
obs : ¬x ∈ range as
this : ⨅ (i : ι), as i = x
⊢ ⋃ (i : ι), Ici (as i) = Ioi x
[PROOFSTEP]
rw [← this] at obs
[GOAL]
α : Type u
β : Type v
ι✝ : Type u_1
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_3
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
obs : ¬⨅ (i : ι), as i ∈ range as
this : ⨅ (i : ι), as i = x
⊢ ⋃ (i : ι), Ici (as i) = Ioi x
[PROOFSTEP]
rw [← this]
[GOAL]
α : Type u
β : Type v
ι✝ : Type u_1
R : Type u_2
inst✝³ : CompleteLinearOrder R
inst✝² : TopologicalSpace R
inst✝¹ : OrderTopology R
ι : Type u_3
x : R
as : ι → R
x_lt : ∀ (i : ι), x < as i
F : Filter ι
inst✝ : NeBot F
as_lim : Tendsto as F (𝓝 x)
obs : ¬⨅ (i : ι), as i ∈ range as
this : ⨅ (i : ι), as i = x
⊢ ⋃ (i : ι), Ici (as i) = Ioi (⨅ (i : ι), as i)
[PROOFSTEP]
exact iUnion_Ici_eq_Ioi_iInf obs
[GOAL]
α : Type u
β : Type v
s : ℕ → Set α
⊢ limsup s atTop = {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop}
[PROOFSTEP]
ext ω
[GOAL]
case h
α : Type u
β : Type v
s : ℕ → Set α
ω : α
⊢ ω ∈ limsup s atTop ↔ ω ∈ {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop}
[PROOFSTEP]
simp only [limsup_eq_iInf_iSup_of_nat, ge_iff_le, Set.iSup_eq_iUnion, Set.iInf_eq_iInter, Set.mem_iInter,
  Set.mem_iUnion, exists_prop]
[GOAL]
case h
α : Type u
β : Type v
s : ℕ → Set α
ω : α
⊢ (∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1) ↔
    ω ∈ {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop}
[PROOFSTEP]
constructor
[GOAL]
case h.mp
α : Type u
β : Type v
s : ℕ → Set α
ω : α
⊢ (∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1) →
    ω ∈ {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop}
[PROOFSTEP]
intro hω
[GOAL]
case h.mp
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
⊢ ω ∈ {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop}
[PROOFSTEP]
refine'
  tendsto_atTop_atTop_of_monotone'
    (fun n m hnm ↦
      Finset.sum_mono_set_of_nonneg (fun i ↦ Set.indicator_nonneg (fun _ _ ↦ zero_le_one) _) (Finset.range_mono hnm))
    _
[GOAL]
case h.mp
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
⊢ ¬BddAbove (Set.range fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω)
[PROOFSTEP]
rintro ⟨i, h⟩
[GOAL]
case h.mp.intro
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
i : ℕ
h : i ∈ upperBounds (Set.range fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω)
⊢ False
[PROOFSTEP]
simp only [mem_upperBounds, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff'] at h
[GOAL]
case h.mp.intro
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
i : ℕ
h : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ i
⊢ False
[PROOFSTEP]
induction' i with k hk
[GOAL]
case h.mp.intro.zero
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
i : ℕ
h✝ : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ i
h : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ Nat.zero
⊢ False
[PROOFSTEP]
obtain ⟨j, hj₁, hj₂⟩ := hω 1
[GOAL]
case h.mp.intro.zero.intro.intro
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
i : ℕ
h✝ : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ i
h : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ Nat.zero
j : ℕ
hj₁ : 1 ≤ j
hj₂ : ω ∈ s j
⊢ False
[PROOFSTEP]
refine' not_lt.2 (h <| j + 1) (lt_of_le_of_lt (Finset.sum_const_zero.symm : 0 = ∑ k in Finset.range (j + 1), 0).le _)
[GOAL]
case h.mp.intro.zero.intro.intro
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
i : ℕ
h✝ : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ i
h : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ Nat.zero
j : ℕ
hj₁ : 1 ≤ j
hj₂ : ω ∈ s j
⊢ ∑ _x in Finset.range (j + 1), 0 < ∑ k in Finset.range (j + 1), Set.indicator (s (k + 1)) 1 ω
[PROOFSTEP]
refine'
  Finset.sum_lt_sum (fun m _ ↦ Set.indicator_nonneg (fun _ _ ↦ zero_le_one) _)
    ⟨j - 1, Finset.mem_range.2 (lt_of_le_of_lt (Nat.sub_le _ _) j.lt_succ_self), _⟩
[GOAL]
case h.mp.intro.zero.intro.intro
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
i : ℕ
h✝ : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ i
h : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ Nat.zero
j : ℕ
hj₁ : 1 ≤ j
hj₂ : ω ∈ s j
⊢ 0 < Set.indicator (s (j - 1 + 1)) 1 ω
[PROOFSTEP]
rw [Nat.sub_add_cancel hj₁, Set.indicator_of_mem hj₂]
[GOAL]
case h.mp.intro.zero.intro.intro
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
i : ℕ
h✝ : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ i
h : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ Nat.zero
j : ℕ
hj₁ : 1 ≤ j
hj₂ : ω ∈ s j
⊢ 0 < OfNat.ofNat 1 ω
[PROOFSTEP]
exact zero_lt_one
[GOAL]
case h.mp.intro.succ
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
i : ℕ
h✝ : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ i
k : ℕ
hk : (∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ k) → False
h : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ Nat.succ k
⊢ False
[PROOFSTEP]
rw [imp_false] at hk
[GOAL]
case h.mp.intro.succ
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
i : ℕ
h✝ : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ i
k : ℕ
hk : ¬∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ k
h : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ Nat.succ k
⊢ False
[PROOFSTEP]
push_neg at hk
[GOAL]
case h.mp.intro.succ
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
i : ℕ
h✝ : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ i
k : ℕ
h : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ Nat.succ k
hk : ∃ a, k < ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
⊢ False
[PROOFSTEP]
obtain ⟨i, hi⟩ := hk
[GOAL]
case h.mp.intro.succ.intro
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
i✝ : ℕ
h✝ : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ i✝
k : ℕ
h : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ Nat.succ k
i : ℕ
hi : k < ∑ k in Finset.range i, Set.indicator (s (k + 1)) 1 ω
⊢ False
[PROOFSTEP]
obtain ⟨j, hj₁, hj₂⟩ := hω (i + 1)
[GOAL]
case h.mp.intro.succ.intro.intro.intro
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
i✝ : ℕ
h✝ : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ i✝
k : ℕ
h : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ Nat.succ k
i : ℕ
hi : k < ∑ k in Finset.range i, Set.indicator (s (k + 1)) 1 ω
j : ℕ
hj₁ : i + 1 ≤ j
hj₂ : ω ∈ s j
⊢ False
[PROOFSTEP]
replace hi : (∑ k in Finset.range i, (s (k + 1)).indicator 1 ω) = k + 1 := le_antisymm (h i) hi
[GOAL]
case h.mp.intro.succ.intro.intro.intro
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
i✝ : ℕ
h✝ : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ i✝
k : ℕ
h : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ Nat.succ k
i j : ℕ
hj₁ : i + 1 ≤ j
hj₂ : ω ∈ s j
hi : ∑ k in Finset.range i, Set.indicator (s (k + 1)) 1 ω = k + 1
⊢ False
[PROOFSTEP]
refine' not_lt.2 (h <| j + 1) _
[GOAL]
case h.mp.intro.succ.intro.intro.intro
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
i✝ : ℕ
h✝ : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ i✝
k : ℕ
h : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ Nat.succ k
i j : ℕ
hj₁ : i + 1 ≤ j
hj₂ : ω ∈ s j
hi : ∑ k in Finset.range i, Set.indicator (s (k + 1)) 1 ω = k + 1
⊢ Nat.succ k < ∑ k in Finset.range (j + 1), Set.indicator (s (k + 1)) 1 ω
[PROOFSTEP]
rw [← Finset.sum_range_add_sum_Ico _ (i.le_succ.trans (hj₁.trans j.le_succ)), hi]
[GOAL]
case h.mp.intro.succ.intro.intro.intro
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
i✝ : ℕ
h✝ : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ i✝
k : ℕ
h : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ Nat.succ k
i j : ℕ
hj₁ : i + 1 ≤ j
hj₂ : ω ∈ s j
hi : ∑ k in Finset.range i, Set.indicator (s (k + 1)) 1 ω = k + 1
⊢ Nat.succ k < k + 1 + ∑ k in Finset.Ico i (Nat.succ j), Set.indicator (s (k + 1)) 1 ω
[PROOFSTEP]
refine' lt_add_of_pos_right _ _
[GOAL]
case h.mp.intro.succ.intro.intro.intro
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
i✝ : ℕ
h✝ : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ i✝
k : ℕ
h : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ Nat.succ k
i j : ℕ
hj₁ : i + 1 ≤ j
hj₂ : ω ∈ s j
hi : ∑ k in Finset.range i, Set.indicator (s (k + 1)) 1 ω = k + 1
⊢ 0 < ∑ k in Finset.Ico i (Nat.succ j), Set.indicator (s (k + 1)) 1 ω
[PROOFSTEP]
rw [(Finset.sum_const_zero.symm : 0 = ∑ k in Finset.Ico i (j + 1), 0)]
[GOAL]
case h.mp.intro.succ.intro.intro.intro
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
i✝ : ℕ
h✝ : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ i✝
k : ℕ
h : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ Nat.succ k
i j : ℕ
hj₁ : i + 1 ≤ j
hj₂ : ω ∈ s j
hi : ∑ k in Finset.range i, Set.indicator (s (k + 1)) 1 ω = k + 1
⊢ ∑ _x in Finset.Ico i (j + 1), 0 < ∑ k in Finset.Ico i (Nat.succ j), Set.indicator (s (k + 1)) 1 ω
[PROOFSTEP]
refine'
  Finset.sum_lt_sum (fun m _ ↦ Set.indicator_nonneg (fun _ _ ↦ zero_le_one) _)
    ⟨j - 1,
      Finset.mem_Ico.2
        ⟨(Nat.le_sub_iff_add_le (le_trans ((le_add_iff_nonneg_left _).2 zero_le') hj₁)).2 hj₁,
          lt_of_le_of_lt (Nat.sub_le _ _) j.lt_succ_self⟩,
      _⟩
[GOAL]
case h.mp.intro.succ.intro.intro.intro
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
i✝ : ℕ
h✝ : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ i✝
k : ℕ
h : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ Nat.succ k
i j : ℕ
hj₁ : i + 1 ≤ j
hj₂ : ω ∈ s j
hi : ∑ k in Finset.range i, Set.indicator (s (k + 1)) 1 ω = k + 1
⊢ 0 < Set.indicator (s (j - 1 + 1)) 1 ω
[PROOFSTEP]
rw [Nat.sub_add_cancel (le_trans ((le_add_iff_nonneg_left _).2 zero_le') hj₁), Set.indicator_of_mem hj₂]
[GOAL]
case h.mp.intro.succ.intro.intro.intro
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
i✝ : ℕ
h✝ : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ i✝
k : ℕ
h : ∀ (a : ℕ), ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω ≤ Nat.succ k
i j : ℕ
hj₁ : i + 1 ≤ j
hj₂ : ω ∈ s j
hi : ∑ k in Finset.range i, Set.indicator (s (k + 1)) 1 ω = k + 1
⊢ 0 < OfNat.ofNat 1 ω
[PROOFSTEP]
exact zero_lt_one
[GOAL]
case h.mpr
α : Type u
β : Type v
s : ℕ → Set α
ω : α
⊢ ω ∈ {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop} →
    ∀ (i : ℕ), ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
[PROOFSTEP]
rintro hω i
[GOAL]
case h.mpr
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ω ∈ {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop}
i : ℕ
⊢ ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
[PROOFSTEP]
rw [Set.mem_setOf_eq, tendsto_atTop_atTop] at hω
[GOAL]
case h.mpr
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (b : ℕ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
i : ℕ
⊢ ∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
[PROOFSTEP]
by_contra hcon
[GOAL]
case h.mpr
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (b : ℕ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
i : ℕ
hcon : ¬∃ i_1, i ≤ i_1 ∧ ω ∈ s i_1
⊢ False
[PROOFSTEP]
push_neg at hcon
[GOAL]
case h.mpr
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (b : ℕ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
i : ℕ
hcon : ∀ (i_1 : ℕ), i ≤ i_1 → ¬ω ∈ s i_1
⊢ False
[PROOFSTEP]
obtain ⟨j, h⟩ := hω (i + 1)
[GOAL]
case h.mpr.intro
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (b : ℕ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
i : ℕ
hcon : ∀ (i_1 : ℕ), i ≤ i_1 → ¬ω ∈ s i_1
j : ℕ
h : ∀ (a : ℕ), j ≤ a → i + 1 ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
⊢ False
[PROOFSTEP]
have : (∑ k in Finset.range j, (s (k + 1)).indicator 1 ω) ≤ i :=
  by
  have hle : ∀ j ≤ i, (∑ k in Finset.range j, (s (k + 1)).indicator 1 ω) ≤ i :=
    by
    refine' fun j hij ↦ (Finset.sum_le_card_nsmul _ _ _ _ : _ ≤ (Finset.range j).card • 1).trans _
    · exact fun m _ ↦ Set.indicator_apply_le' (fun _ ↦ le_rfl) fun _ ↦ zero_le_one
    · simpa only [Finset.card_range, smul_eq_mul, mul_one]
  by_cases hij : j < i
  · exact hle _ hij.le
  · rw [← Finset.sum_range_add_sum_Ico _ (not_lt.1 hij)]
    suffices (∑ k in Finset.Ico i j, (s (k + 1)).indicator 1 ω) = 0
      by
      rw [this, add_zero]
      exact hle _ le_rfl
    refine' Finset.sum_eq_zero fun m hm ↦ _
    exact Set.indicator_of_not_mem (hcon _ <| (Finset.mem_Ico.1 hm).1.trans m.le_succ) _
[GOAL]
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (b : ℕ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
i : ℕ
hcon : ∀ (i_1 : ℕ), i ≤ i_1 → ¬ω ∈ s i_1
j : ℕ
h : ∀ (a : ℕ), j ≤ a → i + 1 ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
⊢ ∑ k in Finset.range j, Set.indicator (s (k + 1)) 1 ω ≤ i
[PROOFSTEP]
have hle : ∀ j ≤ i, (∑ k in Finset.range j, (s (k + 1)).indicator 1 ω) ≤ i :=
  by
  refine' fun j hij ↦ (Finset.sum_le_card_nsmul _ _ _ _ : _ ≤ (Finset.range j).card • 1).trans _
  · exact fun m _ ↦ Set.indicator_apply_le' (fun _ ↦ le_rfl) fun _ ↦ zero_le_one
  · simpa only [Finset.card_range, smul_eq_mul, mul_one]
[GOAL]
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (b : ℕ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
i : ℕ
hcon : ∀ (i_1 : ℕ), i ≤ i_1 → ¬ω ∈ s i_1
j : ℕ
h : ∀ (a : ℕ), j ≤ a → i + 1 ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
⊢ ∀ (j : ℕ), j ≤ i → ∑ k in Finset.range j, Set.indicator (s (k + 1)) 1 ω ≤ i
[PROOFSTEP]
refine' fun j hij ↦ (Finset.sum_le_card_nsmul _ _ _ _ : _ ≤ (Finset.range j).card • 1).trans _
[GOAL]
case refine'_1
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (b : ℕ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
i : ℕ
hcon : ∀ (i_1 : ℕ), i ≤ i_1 → ¬ω ∈ s i_1
j✝ : ℕ
h : ∀ (a : ℕ), j✝ ≤ a → i + 1 ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
j : ℕ
hij : j ≤ i
⊢ ∀ (x : ℕ), x ∈ Finset.range j → Set.indicator (s (x + 1)) 1 ω ≤ 1
[PROOFSTEP]
exact fun m _ ↦ Set.indicator_apply_le' (fun _ ↦ le_rfl) fun _ ↦ zero_le_one
[GOAL]
case refine'_2
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (b : ℕ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
i : ℕ
hcon : ∀ (i_1 : ℕ), i ≤ i_1 → ¬ω ∈ s i_1
j✝ : ℕ
h : ∀ (a : ℕ), j✝ ≤ a → i + 1 ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
j : ℕ
hij : j ≤ i
⊢ Finset.card (Finset.range j) • 1 ≤ i
[PROOFSTEP]
simpa only [Finset.card_range, smul_eq_mul, mul_one]
[GOAL]
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (b : ℕ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
i : ℕ
hcon : ∀ (i_1 : ℕ), i ≤ i_1 → ¬ω ∈ s i_1
j : ℕ
h : ∀ (a : ℕ), j ≤ a → i + 1 ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
hle : ∀ (j : ℕ), j ≤ i → ∑ k in Finset.range j, Set.indicator (s (k + 1)) 1 ω ≤ i
⊢ ∑ k in Finset.range j, Set.indicator (s (k + 1)) 1 ω ≤ i
[PROOFSTEP]
by_cases hij : j < i
[GOAL]
case pos
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (b : ℕ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
i : ℕ
hcon : ∀ (i_1 : ℕ), i ≤ i_1 → ¬ω ∈ s i_1
j : ℕ
h : ∀ (a : ℕ), j ≤ a → i + 1 ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
hle : ∀ (j : ℕ), j ≤ i → ∑ k in Finset.range j, Set.indicator (s (k + 1)) 1 ω ≤ i
hij : j < i
⊢ ∑ k in Finset.range j, Set.indicator (s (k + 1)) 1 ω ≤ i
[PROOFSTEP]
exact hle _ hij.le
[GOAL]
case neg
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (b : ℕ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
i : ℕ
hcon : ∀ (i_1 : ℕ), i ≤ i_1 → ¬ω ∈ s i_1
j : ℕ
h : ∀ (a : ℕ), j ≤ a → i + 1 ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
hle : ∀ (j : ℕ), j ≤ i → ∑ k in Finset.range j, Set.indicator (s (k + 1)) 1 ω ≤ i
hij : ¬j < i
⊢ ∑ k in Finset.range j, Set.indicator (s (k + 1)) 1 ω ≤ i
[PROOFSTEP]
rw [← Finset.sum_range_add_sum_Ico _ (not_lt.1 hij)]
[GOAL]
case neg
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (b : ℕ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
i : ℕ
hcon : ∀ (i_1 : ℕ), i ≤ i_1 → ¬ω ∈ s i_1
j : ℕ
h : ∀ (a : ℕ), j ≤ a → i + 1 ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
hle : ∀ (j : ℕ), j ≤ i → ∑ k in Finset.range j, Set.indicator (s (k + 1)) 1 ω ≤ i
hij : ¬j < i
⊢ ∑ k in Finset.range i, Set.indicator (s (k + 1)) 1 ω + ∑ k in Finset.Ico i j, Set.indicator (s (k + 1)) 1 ω ≤ i
[PROOFSTEP]
suffices (∑ k in Finset.Ico i j, (s (k + 1)).indicator 1 ω) = 0
  by
  rw [this, add_zero]
  exact hle _ le_rfl
[GOAL]
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (b : ℕ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
i : ℕ
hcon : ∀ (i_1 : ℕ), i ≤ i_1 → ¬ω ∈ s i_1
j : ℕ
h : ∀ (a : ℕ), j ≤ a → i + 1 ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
hle : ∀ (j : ℕ), j ≤ i → ∑ k in Finset.range j, Set.indicator (s (k + 1)) 1 ω ≤ i
hij : ¬j < i
this : ∑ k in Finset.Ico i j, Set.indicator (s (k + 1)) 1 ω = 0
⊢ ∑ k in Finset.range i, Set.indicator (s (k + 1)) 1 ω + ∑ k in Finset.Ico i j, Set.indicator (s (k + 1)) 1 ω ≤ i
[PROOFSTEP]
rw [this, add_zero]
[GOAL]
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (b : ℕ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
i : ℕ
hcon : ∀ (i_1 : ℕ), i ≤ i_1 → ¬ω ∈ s i_1
j : ℕ
h : ∀ (a : ℕ), j ≤ a → i + 1 ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
hle : ∀ (j : ℕ), j ≤ i → ∑ k in Finset.range j, Set.indicator (s (k + 1)) 1 ω ≤ i
hij : ¬j < i
this : ∑ k in Finset.Ico i j, Set.indicator (s (k + 1)) 1 ω = 0
⊢ ∑ k in Finset.range i, Set.indicator (s (k + 1)) 1 ω ≤ i
[PROOFSTEP]
exact hle _ le_rfl
[GOAL]
case neg
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (b : ℕ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
i : ℕ
hcon : ∀ (i_1 : ℕ), i ≤ i_1 → ¬ω ∈ s i_1
j : ℕ
h : ∀ (a : ℕ), j ≤ a → i + 1 ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
hle : ∀ (j : ℕ), j ≤ i → ∑ k in Finset.range j, Set.indicator (s (k + 1)) 1 ω ≤ i
hij : ¬j < i
⊢ ∑ k in Finset.Ico i j, Set.indicator (s (k + 1)) 1 ω = 0
[PROOFSTEP]
refine' Finset.sum_eq_zero fun m hm ↦ _
[GOAL]
case neg
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (b : ℕ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
i : ℕ
hcon : ∀ (i_1 : ℕ), i ≤ i_1 → ¬ω ∈ s i_1
j : ℕ
h : ∀ (a : ℕ), j ≤ a → i + 1 ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
hle : ∀ (j : ℕ), j ≤ i → ∑ k in Finset.range j, Set.indicator (s (k + 1)) 1 ω ≤ i
hij : ¬j < i
m : ℕ
hm : m ∈ Finset.Ico i j
⊢ Set.indicator (s (m + 1)) 1 ω = 0
[PROOFSTEP]
exact Set.indicator_of_not_mem (hcon _ <| (Finset.mem_Ico.1 hm).1.trans m.le_succ) _
[GOAL]
case h.mpr.intro
α : Type u
β : Type v
s : ℕ → Set α
ω : α
hω : ∀ (b : ℕ), ∃ i, ∀ (a : ℕ), i ≤ a → b ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
i : ℕ
hcon : ∀ (i_1 : ℕ), i ≤ i_1 → ¬ω ∈ s i_1
j : ℕ
h : ∀ (a : ℕ), j ≤ a → i + 1 ≤ ∑ k in Finset.range a, Set.indicator (s (k + 1)) 1 ω
this : ∑ k in Finset.range j, Set.indicator (s (k + 1)) 1 ω ≤ i
⊢ False
[PROOFSTEP]
exact not_le.2 (lt_of_lt_of_le i.lt_succ_self <| h _ le_rfl) this
[GOAL]
α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
⊢ limsup s atTop = {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop}
[PROOFSTEP]
rw [limsup_eq_tendsto_sum_indicator_nat_atTop s]
[GOAL]
α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
⊢ {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop} =
    {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop}
[PROOFSTEP]
ext ω
[GOAL]
case h
α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
ω : α
⊢ ω ∈ {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop} ↔
    ω ∈ {ω | Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop}
[PROOFSTEP]
simp only [Set.mem_setOf_eq]
[GOAL]
case h
α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
ω : α
⊢ Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop ↔
    Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop
[PROOFSTEP]
rw [(_ :
    (fun n ↦ ∑ k in Finset.range n, (s (k + 1)).indicator (1 : α → R) ω) = fun n ↦
      ↑(∑ k in Finset.range n, (s (k + 1)).indicator (1 : α → ℕ) ω))]
[GOAL]
case h
α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
ω : α
⊢ Tendsto (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) atTop atTop ↔
    Tendsto (fun n => ↑(∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω)) atTop atTop
[PROOFSTEP]
exact tendsto_nat_cast_atTop_iff.symm
[GOAL]
α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
ω : α
⊢ (fun n => ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω) = fun n =>
    ↑(∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω)
[PROOFSTEP]
ext n
[GOAL]
case h
α : Type u
β : Type v
R : Type u_1
inst✝¹ : StrictOrderedSemiring R
inst✝ : Archimedean R
s : ℕ → Set α
ω : α
n : ℕ
⊢ ∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω = ↑(∑ k in Finset.range n, Set.indicator (s (k + 1)) 1 ω)
[PROOFSTEP]
simp only [Set.indicator, Pi.one_apply, Finset.sum_boole, Nat.cast_id]


[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
ι : Type u_3
b : ι → Set E
p : ι → Prop
hbasis : HasBasis (𝓝 0) p b
hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
refine'
  LocallyConvexSpace.ofBases 𝕜 E (fun (x : E) (i : ι) => (· + ·) x '' b i) (fun _ => p) (fun x => _) fun x i hi =>
    (hconvex i hi).translate x
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
ι : Type u_3
b : ι → Set E
p : ι → Prop
hbasis : HasBasis (𝓝 0) p b
hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)
x : E
⊢ HasBasis (𝓝 x) ((fun x => p) x) ((fun x i => (fun x x_1 => x + x_1) x '' b i) x)
[PROOFSTEP]
rw [← map_add_left_nhds_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : TopologicalAddGroup E
ι : Type u_3
b : ι → Set E
p : ι → Prop
hbasis : HasBasis (𝓝 0) p b
hconvex : ∀ (i : ι), p i → Convex 𝕜 (b i)
x : E
⊢ HasBasis (map ((fun x x_1 => x + x_1) x) (𝓝 0)) ((fun x => p) x) ((fun x i => (fun x x_1 => x + x_1) x '' b i) x)
[PROOFSTEP]
exact hbasis.map _
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
[PROOFSTEP]
letI : UniformSpace E := TopologicalAddGroup.toUniformSpace E
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this : UniformSpace E := TopologicalAddGroup.toUniformSpace E
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
[PROOFSTEP]
haveI : UniformAddGroup E := comm_topologicalAddGroup_is_uniform
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this : UniformAddGroup E
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
[PROOFSTEP]
have := (LocallyConvexSpace.convex_open_basis_zero 𝕜 E).comap fun x : E × E => x.2 - x.1
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this :
  HasBasis (comap (fun x => x.snd - x.fst) (𝓝 0)) (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i =>
    (fun x => x.snd - x.fst) ⁻¹' id i
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
[PROOFSTEP]
rw [← uniformity_eq_comap_nhds_zero] at this
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this : HasBasis (uniformity E) (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.snd - x.fst) ⁻¹' id i
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
[PROOFSTEP]
rcases disj.exists_uniform_thickening_of_basis this hs₂ ht₂ with ⟨V, ⟨hV0, hVopen, hVconvex⟩, hV⟩
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this : HasBasis (uniformity E) (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.snd - x.fst) ⁻¹' id i
V : Set E
hV :
  Disjoint (⋃ (x : E) (_ : x ∈ s), UniformSpace.ball x ((fun x => x.snd - x.fst) ⁻¹' id V))
    (⋃ (x : E) (_ : x ∈ t), UniformSpace.ball x ((fun x => x.snd - x.fst) ⁻¹' id V))
hV0 : 0 ∈ V
hVopen : IsOpen V
hVconvex : Convex 𝕜 V
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
[PROOFSTEP]
refine'
  ⟨s + V, t + V, hVopen.add_left, hVopen.add_left, hs₁.add hVconvex, ht₁.add hVconvex, subset_add_left _ hV0,
    subset_add_left _ hV0, _⟩
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this : HasBasis (uniformity E) (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.snd - x.fst) ⁻¹' id i
V : Set E
hV :
  Disjoint (⋃ (x : E) (_ : x ∈ s), UniformSpace.ball x ((fun x => x.snd - x.fst) ⁻¹' id V))
    (⋃ (x : E) (_ : x ∈ t), UniformSpace.ball x ((fun x => x.snd - x.fst) ⁻¹' id V))
hV0 : 0 ∈ V
hVopen : IsOpen V
hVconvex : Convex 𝕜 V
⊢ Disjoint (s + V) (t + V)
[PROOFSTEP]
simp_rw [← iUnion_add_left_image, image_add_left]
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this : HasBasis (uniformity E) (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.snd - x.fst) ⁻¹' id i
V : Set E
hV :
  Disjoint (⋃ (x : E) (_ : x ∈ s), UniformSpace.ball x ((fun x => x.snd - x.fst) ⁻¹' id V))
    (⋃ (x : E) (_ : x ∈ t), UniformSpace.ball x ((fun x => x.snd - x.fst) ⁻¹' id V))
hV0 : 0 ∈ V
hVopen : IsOpen V
hVconvex : Convex 𝕜 V
⊢ Disjoint (⋃ (a : E) (_ : a ∈ s), (fun x => -a + x) ⁻¹' V) (⋃ (a : E) (_ : a ∈ t), (fun x => -a + x) ⁻¹' V)
[PROOFSTEP]
simp_rw [UniformSpace.ball, ← preimage_comp, sub_eq_neg_add] at hV
[GOAL]
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : LinearOrderedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : TopologicalSpace E
inst✝² : TopologicalAddGroup E
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : LocallyConvexSpace 𝕜 E
s t : Set E
disj : Disjoint s t
hs₁ : Convex 𝕜 s
hs₂ : IsCompact s
ht₁ : Convex 𝕜 t
ht₂ : IsClosed t
this✝¹ : UniformSpace E := TopologicalAddGroup.toUniformSpace E
this✝ : UniformAddGroup E
this : HasBasis (uniformity E) (fun s => 0 ∈ s ∧ IsOpen s ∧ Convex 𝕜 s) fun i => (fun x => x.snd - x.fst) ⁻¹' id i
V : Set E
hV0 : 0 ∈ V
hVopen : IsOpen V
hVconvex : Convex 𝕜 V
hV :
  Disjoint (⋃ (x : E) (_ : x ∈ s), (fun x => -x.fst + x.snd) ∘ Prod.mk x ⁻¹' id V)
    (⋃ (x : E) (_ : x ∈ t), (fun x => -x.fst + x.snd) ∘ Prod.mk x ⁻¹' id V)
⊢ Disjoint (⋃ (a : E) (_ : a ∈ s), (fun x => -a + x) ⁻¹' V) (⋃ (a : E) (_ : a ∈ t), (fun x => -a + x) ⁻¹' V)
[PROOFSTEP]
exact hV
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
ts : Set (TopologicalSpace E)
h : ∀ (t : TopologicalSpace E), t ∈ ts → LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
letI : TopologicalSpace E := sInf ts
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
ts : Set (TopologicalSpace E)
h : ∀ (t : TopologicalSpace E), t ∈ ts → LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
refine'
  LocallyConvexSpace.ofBases 𝕜 E (fun _ => fun If : Set ts × (ts → Set E) => ⋂ i ∈ If.1, If.2 i)
    (fun x => fun If : Set ts × (ts → Set E) => If.1.Finite ∧ ∀ i ∈ If.1, If.2 i ∈ @nhds _ (↑i) x ∧ Convex 𝕜 (If.2 i))
    (fun x => _) fun x If hif => convex_iInter fun i => convex_iInter fun hi => (hif.2 i hi).2
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
ts : Set (TopologicalSpace E)
h : ∀ (t : TopologicalSpace E), t ∈ ts → LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
x : E
⊢ HasBasis (𝓝 x)
    ((fun x If => Set.Finite If.fst ∧ ∀ (i : ↑ts), i ∈ If.fst → Prod.snd If i ∈ 𝓝 x ∧ Convex 𝕜 (Prod.snd If i)) x)
    ((fun x If => ⋂ (i : ↑ts) (_ : i ∈ If.fst), Prod.snd If i) x)
[PROOFSTEP]
rw [nhds_sInf, ← iInf_subtype'']
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
ts : Set (TopologicalSpace E)
h : ∀ (t : TopologicalSpace E), t ∈ ts → LocallyConvexSpace 𝕜 E
this : TopologicalSpace E := sInf ts
x : E
⊢ HasBasis (⨅ (i : ↑ts), 𝓝 x)
    ((fun x If => Set.Finite If.fst ∧ ∀ (i : ↑ts), i ∈ If.fst → Prod.snd If i ∈ 𝓝 x ∧ Convex 𝕜 (Prod.snd If i)) x)
    ((fun x If => ⋂ (i : ↑ts) (_ : i ∈ If.fst), Prod.snd If i) x)
[PROOFSTEP]
exact hasBasis_iInf' fun i : ts => (@locallyConvexSpace_iff 𝕜 E _ _ _ ↑i).mp (h (↑i) i.2) x
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
ts' : ι → TopologicalSpace E
h' : ∀ (i : ι), LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
refine' locallyConvexSpace_sInf _
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
ts' : ι → TopologicalSpace E
h' : ∀ (i : ι), LocallyConvexSpace 𝕜 E
⊢ ∀ (t : TopologicalSpace E), (t ∈ range fun i => ts' i) → LocallyConvexSpace 𝕜 E
[PROOFSTEP]
rwa [forall_range_iff]
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
rw [inf_eq_iInf]
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
refine' locallyConvexSpace_iInf fun b => _
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
b : Bool
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
cases b
[GOAL]
case false
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
assumption
[GOAL]
case true
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
t₁ t₂ : TopologicalSpace E
h₁ : LocallyConvexSpace 𝕜 E
h₂ : LocallyConvexSpace 𝕜 E
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
assumption
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
letI : TopologicalSpace E := t.induced f
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (↑f) t
⊢ LocallyConvexSpace 𝕜 E
[PROOFSTEP]
refine'
  LocallyConvexSpace.ofBases 𝕜 E (fun _ => preimage f) (fun x => fun s : Set F => s ∈ 𝓝 (f x) ∧ Convex 𝕜 s) (fun x => _)
    fun x s ⟨_, hs⟩ => hs.linear_preimage f
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (↑f) t
x : E
⊢ HasBasis (𝓝 x) ((fun x s => s ∈ 𝓝 (↑f x) ∧ Convex 𝕜 s) x) ((fun x => preimage ↑f) x)
[PROOFSTEP]
rw [nhds_induced]
[GOAL]
ι : Sort u_1
𝕜 : Type u_2
E : Type u_3
F : Type u_4
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
t : TopologicalSpace F
inst✝ : LocallyConvexSpace 𝕜 F
f : E →ₗ[𝕜] F
this : TopologicalSpace E := induced (↑f) t
x : E
⊢ HasBasis (comap (↑f) (𝓝 (↑f x))) ((fun x s => s ∈ 𝓝 (↑f x) ∧ Convex 𝕜 s) x) ((fun x => preimage ↑f) x)
[PROOFSTEP]
exact (LocallyConvexSpace.convex_basis <| f x).comap f


[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
hd : Summable d
⊢ CauchySeq f
[PROOFSTEP]
refine
  EMetric.cauchySeq_iff_NNReal.2 fun ε εpos =>
    ?_
      -- Actually we need partial sums of `d` to be a Cauchy sequence
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
hd : Summable d
ε : ℝ≥0
εpos : 0 < ε
⊢ ∃ N, ∀ (n : ℕ), N ≤ n → edist (f n) (f N) < ↑ε
[PROOFSTEP]
replace hd : CauchySeq fun n : ℕ => ∑ x in range n, d x :=
  let ⟨_, H⟩ := hd
  H.tendsto_sum_nat.cauchySeq
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x in range n, d x
⊢ ∃ N, ∀ (n : ℕ), N ≤ n → edist (f n) (f N) < ↑ε
[PROOFSTEP]
refine (Metric.cauchySeq_iff'.1 hd ε (NNReal.coe_pos.2 εpos)).imp fun N hN n hn => ?_
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x in range n, d x
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (∑ x in range n, d x) (∑ x in range N, d x) < ↑ε
n : ℕ
hn : N ≤ n
⊢ edist (f n) (f N) < ↑ε
[PROOFSTEP]
specialize hN n hn
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x in range n, d x
N n : ℕ
hn : N ≤ n
hN : dist (∑ x in range n, d x) (∑ x in range N, d x) < ↑ε
⊢ edist (f n) (f N) < ↑ε
[PROOFSTEP]
rw [dist_nndist, NNReal.nndist_eq, ← sum_range_add_sum_Ico _ hn, add_tsub_cancel_left, NNReal.coe_lt_coe, max_lt_iff] at
  hN
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x in range n, d x
N n : ℕ
hn : N ≤ n
hN : ∑ k in Ico N n, d k < ε ∧ ∑ x in range N, d x - (∑ k in range N, d k + ∑ k in Ico N n, d k) < ε
⊢ edist (f n) (f N) < ↑ε
[PROOFSTEP]
rw [edist_comm]
  -- Then use `hf` to simplify the goal to the same form
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x in range n, d x
N n : ℕ
hn : N ≤ n
hN : ∑ k in Ico N n, d k < ε ∧ ∑ x in range N, d x - (∑ k in range N, d k + ∑ k in Ico N n, d k) < ε
⊢ edist (f N) (f n) < ↑ε
[PROOFSTEP]
refine lt_of_le_of_lt (edist_le_Ico_sum_of_edist_le hn fun _ _ => hf _) ?_
[GOAL]
α : Type u_1
inst✝ : PseudoEMetricSpace α
f : ℕ → α
d : ℕ → ℝ≥0
hf : ∀ (n : ℕ), edist (f n) (f (Nat.succ n)) ≤ ↑(d n)
ε : ℝ≥0
εpos : 0 < ε
hd : CauchySeq fun n => ∑ x in range n, d x
N n : ℕ
hn : N ≤ n
hN : ∑ k in Ico N n, d k < ε ∧ ∑ x in range N, d x - (∑ k in range N, d k + ∑ k in Ico N n, d k) < ε
⊢ ∑ i in Ico N n, ↑(d i) < ↑ε
[PROOFSTEP]
exact_mod_cast hN.1
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
hd : Summable d
⊢ CauchySeq f
[PROOFSTEP]
refine' Metric.cauchySeq_iff'.2 fun ε εpos => _
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
hd : Summable d
ε : ℝ
εpos : ε > 0
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → dist (f n) (f N) < ε
[PROOFSTEP]
replace hd : CauchySeq fun n : ℕ => ∑ x in range n, d x :=
  let ⟨_, H⟩ := hd
  H.tendsto_sum_nat.cauchySeq
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
ε : ℝ
εpos : ε > 0
hd : CauchySeq fun n => ∑ x in range n, d x
⊢ ∃ N, ∀ (n : ℕ), n ≥ N → dist (f n) (f N) < ε
[PROOFSTEP]
refine' (Metric.cauchySeq_iff'.1 hd ε εpos).imp fun N hN n hn => _
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
ε : ℝ
εpos : ε > 0
hd : CauchySeq fun n => ∑ x in range n, d x
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (∑ x in range n, d x) (∑ x in range N, d x) < ε
n : ℕ
hn : n ≥ N
⊢ dist (f n) (f N) < ε
[PROOFSTEP]
have hsum := hN n hn
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
ε : ℝ
εpos : ε > 0
hd : CauchySeq fun n => ∑ x in range n, d x
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (∑ x in range n, d x) (∑ x in range N, d x) < ε
n : ℕ
hn : n ≥ N
hsum : dist (∑ x in range n, d x) (∑ x in range N, d x) < ε
⊢ dist (f n) (f N) < ε
[PROOFSTEP]
rw [Real.dist_eq, ← sum_Ico_eq_sub _ hn] at hsum
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
ε : ℝ
εpos : ε > 0
hd : CauchySeq fun n => ∑ x in range n, d x
N : ℕ
hN : ∀ (n : ℕ), n ≥ N → dist (∑ x in range n, d x) (∑ x in range N, d x) < ε
n : ℕ
hn : n ≥ N
hsum : |∑ k in Ico N n, d k| < ε
⊢ dist (f n) (f N) < ε
[PROOFSTEP]
calc
  dist (f n) (f N) = dist (f N) (f n) := dist_comm _ _
  _ ≤ ∑ x in Ico N n, d x := (dist_le_Ico_sum_of_dist_le hn fun _ _ => hf _)
  _ ≤ |∑ x in Ico N n, d x| := (le_abs_self _)
  _ < ε := hsum
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a✝ : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ dist (f n) a ≤ ∑' (m : ℕ), d (n + m)
[PROOFSTEP]
refine' le_of_tendsto (tendsto_const_nhds.dist ha) (eventually_atTop.2 ⟨n, fun m hnm => _⟩)
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a✝ : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ dist (f n) (f m) ≤ ∑' (m : ℕ), d (n + m)
[PROOFSTEP]
refine' le_trans (dist_le_Ico_sum_of_dist_le hnm fun _ _ => hf _) _
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a✝ : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ ∑ i in Ico n m, d i ≤ ∑' (m : ℕ), d (n + m)
[PROOFSTEP]
rw [sum_Ico_eq_sum_range]
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a✝ : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ ∑ k in range (m - n), d (n + k) ≤ ∑' (m : ℕ), d (n + m)
[PROOFSTEP]
refine' sum_le_tsum (range _) (fun _ _ => le_trans dist_nonneg (hf _)) _
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a✝ : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
hd : Summable d
a : α
ha : Tendsto f atTop (𝓝 a)
n m : ℕ
hnm : m ≥ n
⊢ Summable fun k => d (n + k)
[PROOFSTEP]
exact hd.comp_injective (add_right_injective n)
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f (Nat.succ n)) ≤ d n
hd : Summable d
ha : Tendsto f atTop (𝓝 a)
⊢ dist (f 0) a ≤ tsum d
[PROOFSTEP]
simpa only [zero_add] using dist_le_tsum_of_dist_le_of_tendsto d hf hd ha 0
[GOAL]
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
h : Summable fun n => dist (f n) (f (Nat.succ n))
ha : Tendsto f atTop (𝓝 a)
⊢ dist (f 0) a ≤ ∑' (n : ℕ), dist (f n) (f (Nat.succ n))
[PROOFSTEP]
simpa only [zero_add] using dist_le_tsum_dist_of_tendsto h ha 0