continuous_le_rng — Mathlib

English

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

Русский

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

LaTeX

$$$$ t_2 \le t_3 \Rightarrow (\text{Continuous}[t_1,t_2] f) \Rightarrow \text{Continuous}[t_1,t_3] f. $$$$

Lean4

theorem continuous_le_rng {t₁ : TopologicalSpace α} {t₂ t₃ : TopologicalSpace β} (h₁ : t₂ ≤ t₃)
    (h₂ : Continuous[t₁, t₂] f) : Continuous[t₁, t₃] f :=
  by
  rw [continuous_iff_coinduced_le] at h₂ ⊢
  exact le_trans h₂ h₁

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