English
Let t1 be a topology on α and T a set of topologies on β. A map f: α → β is continuous from (α, t1) to the infimum of T if and only if f is continuous from (α, t1) to every t in T.
Русский
Пусть t1 — топология на α, T — множество топологий на β. Отображение f: α → β непрерывно от (α, t1) к inf(T) тогда и только тогда, когда оно непрерывно от (α, t1) к каждой топологии t ∈ T.
LaTeX
$$$\\text{Continuous}_{t_1, \\; \\operatorname{sInf} T} f \\;\\Longleftrightarrow\\; \\forall t \\in T,\\; \\text{Continuous}_{t_1, t} f.$$$
Lean4
theorem continuous_sInf_rng {t₁ : TopologicalSpace α} {T : Set (TopologicalSpace β)} :
Continuous[t₁, sInf T] f ↔ ∀ t ∈ T, Continuous[t₁, t] f := by simp only [continuous_iff_coinduced_le, le_sInf_iff]
