English
A uniform continuous function of two variables remains uniform continuous when viewing as a function on one variable into a product space.
Русский
Равномерно непрерывная функция двух переменных сохраняет свойство, когда рассматривается как функция одной переменной в произведение.
LaTeX
$$$\text{UniformContinuous}(f) \Rightarrow \forall b, \text{UniformContinuous}(a \mapsto (f(a), g(b)))$$$
Lean4
/-- A version of `uniformContinuous_sInf_dom` for binary functions -/
theorem uniformContinuous_sInf_dom₂ {α β γ} {f : α → β → γ} {uas : Set (UniformSpace α)} {ubs : Set (UniformSpace β)}
{ua : UniformSpace α} {ub : UniformSpace β} {uc : UniformSpace γ} (ha : ua ∈ uas) (hb : ub ∈ ubs)
(hf : UniformContinuous fun p : α × β => f p.1 p.2) :
by
haveI := sInf uas; haveI := sInf ubs
exact @UniformContinuous _ _ _ uc fun p : α × β => f p.1 p.2 := by
-- proof essentially copied from `continuous_sInf_dom`
let _ : UniformSpace (α × β) := instUniformSpaceProd
have ha := uniformContinuous_sInf_dom ha uniformContinuous_id
have hb := uniformContinuous_sInf_dom hb uniformContinuous_id
have h_unif_cont_id := @UniformContinuous.prodMap _ _ _ _ (sInf uas) (sInf ubs) ua ub _ _ ha hb
exact @UniformContinuous.comp _ _ _ (id _) (id _) _ _ _ hf h_unif_cont_id
