continuous_iff_le_induced — Mathlib

English

For f: α → β and t1 on α, t2 on β, the map f is continuous exactly when t1 ≤ induced f t2.

Русский

Для отображения f: α → β и топологий t1 на α и t2 на β отображение f непрерывно тогда и только тогда, когда t1 ⩽ induced f t2.

LaTeX

$$$$ Continuous[t_1, t_2] f \iff t_1 \le \mathrm{induced}(f,t_2). $$$$

Lean4

theorem continuous_iff_le_induced {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β} :
    Continuous[t₁, t₂] f ↔ t₁ ≤ induced f t₂ :=
  Iff.trans continuous_iff_coinduced_le (gc_coinduced_induced f _ _)

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