English
From a UniformContinuous₂ f, the corresponding uncurry f is uniformly continuous.
Русский
Из UniformContinuous₂ f следует, что uncurry f равномерно непрерывна.
LaTeX
$$$UniformContinuous\₂ \; f \Rightarrow UniformContinuous(\text{uncurry } f)$$$
Lean4
/-- A version of `UniformContinuous.inf_dom_right` for binary functions -/
theorem uniformContinuous_inf_dom_right₂ {α β γ} {f : α → β → γ} {ua1 ua2 : UniformSpace α} {ub1 ub2 : UniformSpace β}
{uc1 : UniformSpace γ} (h : by haveI := ua2; haveI := ub2; exact UniformContinuous fun p : α × β => f p.1 p.2) :
by
haveI := ua1 ⊓ ua2; haveI := ub1 ⊓ ub2
exact UniformContinuous fun p : α × β => f p.1 p.2 := by
-- proof essentially copied from `continuous_inf_dom_right₂`
have ha := @UniformContinuous.inf_dom_right _ _ id ua1 ua2 ua2 (@uniformContinuous_id _ (id _))
have hb := @UniformContinuous.inf_dom_right _ _ id ub1 ub2 ub2 (@uniformContinuous_id _ (id _))
have h_unif_cont_id := @UniformContinuous.prodMap _ _ _ _ (ua1 ⊓ ua2) (ub1 ⊓ ub2) ua2 ub2 _ _ ha hb
exact @UniformContinuous.comp _ _ _ (id _) (id _) _ _ _ h h_unif_cont_id
