English
If nets y and z converge to x, and a predicate r holds asymptotically along the product net, then for almost every index the segments between y and z satisfy r pointwise.
Русский
Если сетки y и z сходятся к x, и для почти всех индексов выполняется условие r на пару p = (y, z), то почти для каждого индекса χ множество векторов на отрезке между y(χ) и z(χ) удовлетворяют r.
LaTeX
$$Let hy: Tendsto y f (nhds x) and hz: Tendsto z f (nhds x) and hr: ∀ᶠ p in f × nhds x, r p.1 p.2. Then ∀ᶠ χ in f, ∀ v ∈ [y χ -[\\mathbb{R}] z χ], r χ v.$$
Lean4
theorem segment_of_prod_nhds (hy : Tendsto y f (𝓝 x)) (hz : Tendsto z f (𝓝 x)) (hr : ∀ᶠ p in f ×ˢ 𝓝 x, r p.1 p.2) :
∀ᶠ χ in f, ∀ v ∈ [y χ -[ℝ] z χ], r χ v :=
by
obtain ⟨p, hp, δ, hδ, hr⟩ := eventually_prod_nhds_iff.mp hr
rw [Metric.tendsto_nhds] at hy hz
filter_upwards [hp, hy δ hδ, hz δ hδ] with χ hp hy hz
exact fun v hv => hr hp <| convex_iff_segment_subset.mp (convex_ball x δ) hy hz hv
