continuous_induced_dom — Mathlib

English

For f: α → β and a topology t on β, the map f is continuous from (α, induced f t) to (β, t).

Русский

Для отображения f: α → β и топологии t на β отображение f непрерывно из тангенса (α, induced f t) в (β, t).

LaTeX

$$$$ \text{Continuous}[\mathrm{induced}(f,t),t]\ f. $$$$

Lean4

@[continuity, fun_prop]
theorem continuous_induced_dom {t : TopologicalSpace β} : Continuous[induced f t, t] f :=
  continuous_iff_le_induced.2 le_rfl

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