continuous_iSup_dom — Mathlib

English

Let t1 be a family of topologies indexed by iota, and t2 a topology on β. Then Continuous[iSup t1, t2] f iff ∀ i, Continuous[t1 i, t2] f.

Русский

Пусть t1 задаётся индексированным семейством топологий, а t2 — топология на β. Тогда Continuous[iSup t1, t2] f эквивалентно ∀ i, Continuous[t1 i, t2] f.

LaTeX

$$$$ \text{Continuous}[\mathrm{iSup}(t_1), t_2] f \iff \forall i, \text{Continuous}[t_1(i), t_2] f. $$$$

Lean4

theorem continuous_iSup_dom {t₁ : ι → TopologicalSpace α} {t₂ : TopologicalSpace β} :
    Continuous[iSup t₁, t₂] f ↔ ∀ i, Continuous[t₁ i, t₂] f := by simp only [continuous_iff_le_induced, iSup_le_iff]

Похожие утверждения