English
If x IsSt r and y IsSt s, then for any f : R → R → R that is continuous at (r,s), IsSt (x.map₂ f y) (f r s).
Русский
Если x ⪯ r и y ⪯ s, то для любого f: R×R → R непрерывного в (r,s) IsSt (x.map₂ f y) (f r s).
LaTeX
$$$\forall {x y:\mathbb{R}^*} {r s:\mathbb{R}}, \; x.IsSt r \to y.IsSt s \to ∀ f:\mathbb{R}\to\mathbb{R}\to\mathbb{R}, \; \mathrm{ContinuousAt}(\mathrm{uncurry}\ f) (r,s) \rightarrow \mathrm{IsSt}(\mathrm{Filter.Germ.map₂}\ f\ x\ y, f r s)$$$
Lean4
theorem map₂ {x y : ℝ*} {r s : ℝ} (hxr : IsSt x r) (hys : IsSt y s) {f : ℝ → ℝ → ℝ}
(hf : ContinuousAt (Function.uncurry f) (r, s)) : IsSt (x.map₂ f y) (f r s) :=
by
rcases ofSeq_surjective x with ⟨x, rfl⟩
rcases ofSeq_surjective y with ⟨y, rfl⟩
rw [isSt_ofSeq_iff_tendsto] at hxr hys
exact isSt_ofSeq_iff_tendsto.2 <| hf.tendsto.comp (hxr.prodMk_nhds hys)
