English
Let f: α → β → γ. If a ∈ sα and f.uncurry is ContinuousOn on sα ×ˢ sβ, then the section a ↦ f(a,·) is continuous on sβ.
Русский
Пусть f: α → β → γ. Если a ∈ sα и f.uncurry непрерывна на sα ×ˢ sβ, то секция a ↦ f(a,·) непрерывна на sβ.
LaTeX
$$$$a\in s_\alpha \; \wedge\; \text{ContinuousOn}(f.\text{uncurry},
s_\alpha \times\! s_\beta) \Rightarrow \text{ContinuousOn}(\lambda b, f(a,b)) s_\beta.$$$$
Lean4
theorem uncurry_right {f : α → β → γ} {sα : Set α} {sβ : Set β} (b : β) (ha : b ∈ sβ)
(h : ContinuousOn f.uncurry (sα ×ˢ sβ)) : ContinuousOn (fun a => f a b) sα :=
by
let g : α → γ := f.uncurry ∘ (fun a => (a, b))
refine ContinuousOn.congr (f := g) ?_ (fun y => by simp [g])
exact ContinuousOn.comp h (by fun_prop) (by grind [Set.MapsTo])
