continuous_iInf_dom — Mathlib

English

Let t1 be a family of topologies on α, t2 a topology on β, and i an index. If f is continuous from (α, t1 i) to (β, t2), then f is continuous from (α, iInf t1) to (β, t2).

Русский

Пусть {t1i} — семейство топологий на α, t2 — топология на β, и i индекс. Если f непрерывна от (α, t1i) к (β, t2), то она непрерывна от (α, iInf t1) к (β, t2).

LaTeX

$$$\\text{Continuous}_{t_1 i, t_2} f \\Rightarrow \\text{Continuous}_{\\mathrm{iInf}\\, t_1, t_2} f.$$$

Lean4

theorem continuous_iInf_dom {t₁ : ι → TopologicalSpace α} {t₂ : TopologicalSpace β} {i : ι} :
    Continuous[t₁ i, t₂] f → Continuous[iInf t₁, t₂] f :=
  continuous_le_dom <| iInf_le _ _

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