continuous_sup_rng_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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