English
Let f: β → α → γ and s: β → α be such that the map (β × α) → γ sending (x, a) to f x a is continuous on the whole product when restricted to univ × [0,1], and s is continuous as a map β → α, and for every x we have f x 0 = f x 1. Then the function β → γ given by x ↦ f x (fract (s x)) is continuous.
Русский
Пусть f: β → α → γ и s: β → α таковы, что отображение (x, a) ↦ f x a непрерывно на всю пару (β, α) при ограничении на univ × [0,1], при этом s непрерывно, и для каждого x выполняется f x 0 = f x 1. Тогда функция x ↦ f x (fract (s x)) непрерывна.
LaTeX
$$$\bigl(\mathrm{ContinuousOn}(\mathrm{uncurry}\ f)\, (\mathrm{univ} \times \mathrm{Icc}(0,1)) \bigr) \land \mathrm{Continuous}\ s \land \bigl(\forall x, f\,x\,0 = f\,x\,1\bigr) \Rightarrow \mathrm{Continuous}\bigl(x \mapsto f\,x\bigl(\operatorname{fract}(s\,x)\bigr)\bigr).$$$
Lean4
theorem comp_fract {s : β → α} {f : β → α → γ} (h : ContinuousOn (uncurry f) <| univ ×ˢ Icc 0 1) (hs : Continuous s)
(hf : ∀ s, f s 0 = f s 1) : Continuous fun x : β => f x <| Int.fract (s x) :=
(h.comp_fract' hf).comp (continuous_id.prodMk hs)
