coinduced_continuous — Mathlib

English

For any f: R → S, the map f is continuous from the given topology on R to the coinduced topology on S.

Русский

Для отображения f: R → S непрерывность сохраняется при переходе к коиндуцированной топологии на S.

LaTeX

$$Continuous f$$

Lean4

theorem coinduced_continuous {R S : Type*} [t : TopologicalSpace R] [Ring S] (f : R → S) :
    Continuous[t, (coinduced f).toTopologicalSpace] f :=
  continuous_sInf_rng.2 <| forall_mem_image.2 fun _ => continuous_iff_coinduced_le.2

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