English
Let t1 be a topology on α and t2i a family of topologies on β indexed by i. The map f is continuous from (α, t1) to the infimum iInf t2 if and only if it is continuous from (α, t1) to every t2i.
Русский
Пусть t1 — топология на α, t2i — множество топологий на β, индексируемых i. Тогда отображение f непрерывно от (α, t1) к iInf t2 тогда и только тогда, когда оно непрерывно к каждому t2i.
LaTeX
$$$\\text{Continuous}_{t_1, \\; \\mathrm{iInf}\\, t_2} f \\;\\iff\\; \\forall i,\\; \\text{Continuous}_{t_1, t_2 i} f.$$$
Lean4
theorem continuous_iInf_rng {t₁ : TopologicalSpace α} {t₂ : ι → TopologicalSpace β} :
Continuous[t₁, iInf t₂] f ↔ ∀ i, Continuous[t₁, t₂ i] f := by simp only [continuous_iff_coinduced_le, le_iInf_iff]
