feat(analysis/topological_structures): add tendsto_of_tendsto_of_tendsto_of_le_of_le

Author: johoelzl

analysis/ennreal.lean

@@ -913,15 +913,15 @@ section tsum
 variables {α : Type*} {β : Type*} {f g : α → ennreal}
 
 protected lemma is_sum : is_sum f (⨆s:finset α, s.sum f) :=
-tendsto_orderable
-  (assume a' ha',
+tendsto_orderable.2
+  ⟨assume a' ha',
     let ⟨s, hs⟩ := lt_supr_iff.mp ha' in
-    mem_at_top_sets.mpr ⟨s, assume t ht, lt_of_lt_of_le hs $ finset.sum_le_sum_of_subset ht⟩)
-  (assume a' ha',
+    mem_at_top_sets.mpr ⟨s, assume t ht, lt_of_lt_of_le hs $ finset.sum_le_sum_of_subset ht⟩,
+  assume a' ha',
     univ_mem_sets' $ assume s,
     have s.sum f ≤ ⨆(s : finset α), s.sum f,
       from le_supr (λ(s : finset α), s.sum f) s,
-    lt_of_le_of_lt this ha')
+    lt_of_le_of_lt this ha'⟩
 
 @[simp] protected lemma has_sum : has_sum f := ⟨_, ennreal.is_sum⟩
 

analysis/topology/topological_structures.lean

@@ -338,13 +338,22 @@ from le_antisymm
     | _, h, (or.inr rfl) := inf_le_right_of_le $ infi_le_of_le b $ infi_le _ h
     end)
 
-lemma tendsto_orderable {f : β → α} {a : α} {x : filter β}
-  (h₁ : ∀a'<a, {b | a' < f b } ∈ x.sets) (h₂ : ∀a'>a, {b | a' > f b } ∈ x.sets) :
-  tendsto f x (nhds a) :=
-by rw [@nhds_eq_orderable α _ _];
-from tendsto_inf.2
-  ⟨tendsto_infi.2 $ assume b, tendsto_infi.2 $ assume hb, tendsto_principal.2 $ h₁ b hb,
-   tendsto_infi.2 $ assume b, tendsto_infi.2 $ assume hb, tendsto_principal.2 $ h₂ b hb⟩
+lemma tendsto_orderable {f : β → α} {a : α} {x : filter β} :
+  tendsto f x (nhds a) ↔ (∀a'<a, {b | a' < f b} ∈ x.sets) ∧ (∀a'>a, {b | a' > f b} ∈ x.sets) :=
+by simp [@nhds_eq_orderable α _ _, tendsto_inf, tendsto_infi, tendsto_principal]
+
+/-- Also known as squeez or sandwich theorem. -/
+lemma tendsto_of_tendsto_of_tendsto_of_le_of_le {f g h : β → α} {b : filter β} {a : α} (hb : b ≠ ⊥)
+  (hg : tendsto g b (nhds a)) (hh : tendsto h b (nhds a))
+  (hgf : {b | g b ≤ f b} ∈ b.sets) (hfh : {b | f b ≤ h b} ∈ b.sets) :
+  tendsto f b (nhds a) :=
+tendsto_orderable.2
+  ⟨assume a' h',
+    have {b : β | a' < g b} ∈ b.sets, from (tendsto_orderable.1 hg).left a' h',
+    by filter_upwards [this, hgf] assume a, lt_of_lt_of_le,
+    assume a' h',
+    have {b : β | h b < a'} ∈ b.sets, from (tendsto_orderable.1 hh).right a' h',
+    by filter_upwards [this, hfh] assume a h₁ h₂, lt_of_le_of_lt h₂ h₁⟩
 
 lemma nhds_orderable_unbounded {a : α} (hu : ∃u, a < u) (hl : ∃l, l < a) :
   nhds a = (⨅l (h₂ : l < a) u (h₂ : a < u), principal {x | l < x ∧ x < u }) :=