continuous_sup_rng_right — Mathlib

English

If f is continuous from t1 to t3, then f is continuous from t1 to t2 ⊔ t3.

Русский

Если f непрерывна от t1 к t3, то она непрерывна от t1 к t2 ⊔ t3.

LaTeX

$$$$ \text{Continuous}[t_1,t_3] f \Rightarrow \text{Continuous}[t_1, t_2 \lor t_3] f. $$$$

Lean4

theorem continuous_sup_rng_right {t₁ : TopologicalSpace α} {t₃ t₂ : TopologicalSpace β} :
    Continuous[t₁, t₃] f → Continuous[t₁, t₂ ⊔ t₃] f :=
  continuous_le_rng le_sup_right

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