continuous_sup_dom — Mathlib

English

A function f is continuous from t1 ⊔ t2 to t3 if and only if it is continuous from t1 to t3 and from t2 to t3.

Русский

Функция f непрерывна от t1 ⊔ t2 к t3 тогда и только тогда, когда она непрерывна от t1 к t3 и от t2 к t3.

LaTeX

$$$$ \text{Continuous}[t_1 \lor t_2, t_3] f \iff (\text{Continuous}[t_1,t_3] f \land \text{Continuous}[t_2,t_3] f). $$$$

Lean4

theorem continuous_sup_dom {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} :
    Continuous[t₁ ⊔ t₂, t₃] f ↔ Continuous[t₁, t₃] f ∧ Continuous[t₂, t₃] f := by
  simp only [continuous_iff_le_induced, sup_le_iff]

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