English
If f1, f2, f3: β → α satisfy Tendsto (x ↦ (f1 x, f2 x)) l (𝓤 α) and Tendsto (x ↦ (f2 x, f3 x)) l (𝓤 α), then Tendsto (x ↦ (f1 x, f3 x)) l (𝓤 α).
Русский
Пусть f1, f2, f3: β → α удовлетворяют, что пары (f1 x, f2 x) и (f2 x, f3 x) сходятся по 𝓤 α при Tendsto, тогда (f1 x, f3 x) сходятся по 𝓤 α.
LaTeX
$$$$\\forall {l} {f_1 f_2 f_3: \\beta \\to \\alpha},\\;\\big(\\mathrm{Tendsto}(x \\mapsto (f_1 x, f_2 x))\\, l\\, (𝓤 \\alpha)\\big) \\to \\big(\\mathrm{Tendsto}(x \\mapsto (f_2 x, f_3 x))\\, l\\, (𝓤 \\alpha)\\big) \\to \\mathrm{Tendsto}(x \\mapsto (f_1 x, f_3 x))\\, l\\, (𝓤 \\alpha).$$$$
Lean4
/-- Relation `fun f g ↦ Tendsto (fun x ↦ (f x, g x)) l (𝓤 α)` is transitive. -/
theorem uniformity_trans {l : Filter β} {f₁ f₂ f₃ : β → α} (h₁₂ : Tendsto (fun x => (f₁ x, f₂ x)) l (𝓤 α))
(h₂₃ : Tendsto (fun x => (f₂ x, f₃ x)) l (𝓤 α)) : Tendsto (fun x => (f₁ x, f₃ x)) l (𝓤 α) :=
by
refine le_trans (le_lift'.2 fun s hs => mem_map.2 ?_) comp_le_uniformity
filter_upwards [mem_map.1 (h₁₂ hs), mem_map.1 (h₂₃ hs)] with x hx₁₂ hx₂₃ using ⟨_, hx₁₂, hx₂₃⟩
