continuous_le_dom — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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