English
If f: X → Y → Z is continuous in the product topology ta1 × tb1, then f is continuous with respect to ta1 ⊓ ta2 on X and tb1 ⊓ tb2 on Y.
Русский
Если f: X → Y → Z непрерывна в произведении топологий ta1 × tb1, то непрерывна и в инфимумах ta1 ⊓ ta2 на X и tb1 ⊓ tb2 на Y.
LaTeX
$$Continuous (λ p:X×Y, f p.1 p.2) → Continuous (λ p:X×Y, f p.1 p.2) (в топологиях ta1⊓ta2, tb1⊓tb2)$$
Lean4
/-- A version of `continuous_inf_dom_right` for binary functions -/
theorem continuous_inf_dom_right₂ {X Y Z} {f : X → Y → Z} {ta1 ta2 : TopologicalSpace X} {tb1 tb2 : TopologicalSpace Y}
{tc1 : TopologicalSpace Z} (h : by haveI := ta2; haveI := tb2; 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_right _ _ id ta1 ta2 ta2 (@continuous_id _ (id _))
have hb := @continuous_inf_dom_right _ _ id tb1 tb2 tb2 (@continuous_id _ (id _))
have h_continuous_id := @Continuous.prodMap _ _ _ _ ta2 tb2 (ta1 ⊓ ta2) (tb1 ⊓ tb2) _ _ ha hb
exact @Continuous.comp _ _ _ (id _) (id _) _ _ _ h h_continuous_id
