continuous_sSup_dom — Mathlib

English

Let T be a set of topologies on α and t2 a topology on β. Then f is continuous from sSup T to t2 iff f is continuous from every t ∈ T to t2.

Русский

Пусть T — множество топологий на α и t2 — топология на β. Тогда f непрерывна от sSup T к t2 тогда и только тогда, когда она непрерывна от каждого t ∈ T к t2.

LaTeX

$$$$ \text{Continuous}[\mathrm{sSup}(T), t_2] f \iff \forall t \in T, \text{Continuous}[t,t_2] f. $$$$

Lean4

theorem continuous_sSup_dom {T : Set (TopologicalSpace α)} {t₂ : TopologicalSpace β} :
    Continuous[sSup T, t₂] f ↔ ∀ t ∈ T, Continuous[t, t₂] f := by simp only [continuous_iff_le_induced, sSup_le_iff]

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