continuous_coinduced_rng — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem continuous_coinduced_rng {t : TopologicalSpace α} : Continuous[t, coinduced f t] f :=
  continuous_iff_coinduced_le.2 le_rfl

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