English
Let t1 be a set of topologies on α, t2 a topology on β, and t ∈ t1. If f: α → β is continuous from (α, t) to (β, t2), then f is continuous from (α, sInf t1) to (β, t2). In particular, continuity survives when the domain topology is replaced by the infimum of a family that contains a given topology in the family.
Русский
Пусть t1 — множество топологий на α, t2 — топология на β, и t ∈ t1. Если f: α → β непрерывна от (α, t) к (β, t2), то f непрерывна от (α, sInf t1) к (β, t2). Непрерывность сохраняется, если область определения снабдить инфимумом семейства топологий, содержащее данную топологию.
LaTeX
$$$\\forall t_1 \\subseteq \\text{Top}(\\alpha),\\; \\forall t_2 \\in \\text{Top}(\\beta),\\; \\forall t \\in t_1,\\quad \\big(\\text{Continuous}_{t,t_2} f \\Rightarrow \\text{Continuous}_{\\operatorname{sInf} t_1,t_2} f\\big).$$$
Lean4
theorem continuous_sInf_dom {t₁ : Set (TopologicalSpace α)} {t₂ : TopologicalSpace β} {t : TopologicalSpace α}
(h₁ : t ∈ t₁) : Continuous[t, t₂] f → Continuous[sInf t₁, t₂] f :=
continuous_le_dom <| sInf_le h₁
