continuous_iSup_rng — Mathlib

English

If f is continuous from t1 to t2(i) for some i, then f is continuous from t1 to iSup t2.

Русский

Если f непрерывна от t1 к t2(i) для некоторого i, то она непрерывна от t1 к iSup t2.

LaTeX

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

Lean4

theorem continuous_iSup_rng {t₁ : TopologicalSpace α} {t₂ : ι → TopologicalSpace β} {i : ι}
    (h : Continuous[t₁, t₂ i] f) : Continuous[t₁, iSup t₂] f :=
  continuous_sSup_rng ⟨i, rfl⟩ h

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