English
If f: X → Y → Z is continuous when X and Y have topologies from tas and tbs, and tX ∈ tas, tY ∈ tbs, then f is continuous under the infimum topologies sInf tas and sInf tbs.
Русский
Если f: X → Y → Z непрерывна при некоторых топологиях из tas и tbs, где tX ∈ tas и tY ∈ tbs, то она непрерывна и под инфимумами tas и tbs.
LaTeX
$$Set.instMembership.mem tas tX → Set.instMembership.mem tbs tY → (Continuous fun p => f p.1 p.2) → Continuous fun p => f p.1 p.2$$
Lean4
/-- A version of `continuous_sInf_dom` for binary functions -/
theorem continuous_sInf_dom₂ {X Y Z} {f : X → Y → Z} {tas : Set (TopologicalSpace X)} {tbs : Set (TopologicalSpace Y)}
{tX : TopologicalSpace X} {tY : TopologicalSpace Y} {tc : TopologicalSpace Z} (hX : tX ∈ tas) (hY : tY ∈ tbs)
(hf : Continuous fun p : X × Y => f p.1 p.2) : by
haveI := sInf tas; haveI := sInf tbs
exact @Continuous _ _ _ tc fun p : X × Y => f p.1 p.2 :=
by
have hX := continuous_sInf_dom hX continuous_id
have hY := continuous_sInf_dom hY continuous_id
have h_continuous_id := @Continuous.prodMap _ _ _ _ tX tY (sInf tas) (sInf tbs) _ _ hX hY
exact @Continuous.comp _ _ _ (id _) (id _) _ _ _ hf h_continuous_id
