continuous_sSup_rng — Mathlib

English

If a topology t is a member of a set t2 and f is continuous to t, then f is continuous to sSup t2.

Русский

Если t ∈ t2 и f непрерывна к t, то f непрерывна к sSup t2.

LaTeX

$$$$ (t \in t_2) \Rightarrow (\text{Continuous}[t_1,t] f) \Rightarrow \text{Continuous}[t_1, \mathrm{sSup}(t_2)] f. $$$$

Lean4

theorem continuous_sSup_rng {t₁ : TopologicalSpace α} {t₂ : Set (TopologicalSpace β)} {t : TopologicalSpace β}
    (h₁ : t ∈ t₂) (hf : Continuous[t₁, t] f) : Continuous[t₁, sSup t₂] f :=
  continuous_iff_coinduced_le.2 <| le_sSup_of_le h₁ <| continuous_iff_coinduced_le.1 hf

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