English
Binary continuity: If a binary function f: X → Y → Z is continuous in the product topology, then under refined product topologies ta1 ⊓ ta2 and tb1 ⊓ tb2, the map p ↦ f(p.1, p.2) remains continuous.
Русский
Двоичную непрерывность: если функция f: X → Y → Z непрерывна в произведенной топологии, то при уточненных топологиях произведение остаётся непрерывной.
LaTeX
$$$\text{Continuous}(p \mapsto f(p.fst, p.snd)) \rightarrow \text{Continuous}(p \mapsto f(p.fst, p.snd))$$$
Lean4
/-- A version of `continuous_inf_dom_left` for binary functions -/
theorem continuous_inf_dom_left₂ {X Y Z} {f : X → Y → Z} {ta1 ta2 : TopologicalSpace X} {tb1 tb2 : TopologicalSpace Y}
{tc1 : TopologicalSpace Z} (h : by haveI := ta1; haveI := tb1; exact Continuous fun p : X × Y => f p.1 p.2) : by
haveI := ta1 ⊓ ta2; haveI := tb1 ⊓ tb2; exact Continuous fun p : X × Y => f p.1 p.2 :=
by
have ha := @continuous_inf_dom_left _ _ id ta1 ta2 ta1 (@continuous_id _ (id _))
have hb := @continuous_inf_dom_left _ _ id tb1 tb2 tb1 (@continuous_id _ (id _))
have h_continuous_id := @Continuous.prodMap _ _ _ _ ta1 tb1 (ta1 ⊓ ta2) (tb1 ⊓ tb2) _ _ ha hb
exact @Continuous.comp _ _ _ (id _) (id _) _ _ _ h h_continuous_id
