continuous_iff_coinduced_le — Mathlib

English

For f: α → β and topologies t1 on α, t2 on β, the map f is continuous exactly when the coinduced topology on α is ≤ t2; i.e., Continuous[t1, t2] f ↔ coinduced f t1 ≤ t2.

Русский

Для отображения f: α → β и топологий t1 на α, t2 на β отображение f непрерывно тогда и только тогда, когда коиндуцированная топология на α ограничивает t2; то есть Continuous[t1, t2] f ⇔ coinduced f t1 ≤ t2.

LaTeX

$$$$ Continuous[t_1, t_2] f \iff \ coinduced(f,t_1) \le t_2. $$$$

Lean4

theorem continuous_iff_coinduced_le {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β} :
    Continuous[t₁, t₂] f ↔ coinduced f t₁ ≤ t₂ :=
  continuous_def

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