Theorems · Theorem · general topology
squeeze_zero
∀ {α : Type u_3} {f g : α → ℝ} {t₀ : Filter α},
(∀ (t : α), 0 ≤ f t) → (∀ (t : α), f t ≤ g t) → Filter.Tendsto g t₀ (nhds 0) → Filter.Tendsto f t₀ (nhds 0)Special case of the sandwich lemma; see tendsto_of_tendsto_of_tendsto_of_le_of_le
and tendsto_of_tendsto_of_tendsto_of_le_of_le' for the general case.
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 117 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- Filterstatement and proof · cited by 8,121
- nhdsstatement and proof · cited by 5,554
- Filter.Tendstostatement and proof · cited by 3,814
- Filter.Eventually.of_forallproof · cited by 526
- squeeze_zero'proof · cited by 8
Cited by16
Results whose statement or proof uses this declaration.
- ApproximatesLinearOn.surjOn_closedBall_of_nonlinearRightInverseproof · cited by 3
- ContinuousLinearMap.exists_preimage_norm_leproof · cited by 2
- AbsolutelyContinuousOnInterval.negproof · cited by 2
- Complex.continuousAt_cpow_zero_of_re_posproof · cited by 2
- CircleDeg1Lift.tendsto_translationNumber_of_dist_bounded_auxproof · cited by 2
- AbsolutelyContinuousOnInterval.addproof · cited by 2
- BoundedContinuousFunction.exists_extension_norm_eq_of_isClosedEmbedding'proof · cited by 2
- Real.hasSum_pow_div_log_of_abs_lt_oneproof · cited by 1
- AbsolutelyContinuousOnInterval.const_smulproof · cited by 1
- aemeasurable_of_unif_approxproof · cited by 1
- exists_nat_nat_continuous_surjective_of_completeSpaceproof · cited by 1