English
If y and z converge to x, and r holds on pairs asymptotically with respect to another filter, and the segments between yχ and zχ stay inside a set s, then r holds along those segments for χ in the filter.
Русский
Если y и z сходятся в x, и условие r выполняется почти всюду на пары, и отрезки между yχ и zχ лежат внутри множества s, то r выполняется на этих отрезках для χ в фильтре.
LaTeX
$$Let hy: Tendsto y f (nhds x) and hz: Tendsto z f (nhds x) and hr: ∀ᶠ p in f × nhds[x] s, r p.1 p.2 and seg: ∀ᶠ χ in f, [y χ -[\\mathbb{R}] z χ] ⊆ s. Then ∀ᶠ χ in f, ∀ v ∈ [y χ -[\\mathbb{R}] z χ], r χ v.$$
Lean4
theorem segment_of_prod_nhdsWithin (hy : Tendsto y f (𝓝 x)) (hz : Tendsto z f (𝓝 x))
(hr : ∀ᶠ p in f ×ˢ 𝓝[s] x, r p.1 p.2) (seg : ∀ᶠ χ in f, [y χ -[ℝ] z χ] ⊆ s) :
∀ᶠ χ in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v :=
by
refine seg.mp <| .mono ?_ (fun _ => forall₂_imp)
apply Eventually.segment_of_prod_nhds hy hz
simpa [nhdsWithin, prod_eq_inf, ← inf_assoc, eventually_inf_principal] using hr
