continuous_uliftMap — Mathlib

English

If f: X → Y is continuous, then ULift.map f: ULift X → ULift Y is continuous.

Русский

Если f: X → Y непрерывно, то ULift.map f: ULift X → ULift Y тоже непрерывно.

LaTeX

$$$(hf : \mathrm{Continuous}(f)) \Rightarrow \mathrm{Continuous}(\mathrm{ULift.map} f).$$$

Lean4

@[continuity, fun_prop]
theorem continuous_uliftMap [TopologicalSpace X] [TopologicalSpace Y] (f : X → Y) (hf : Continuous f) :
    Continuous (ULift.map f : ULift.{u'} X → ULift.{v'} Y) :=
  by
  change Continuous (ULift.up ∘ f ∘ ULift.down)
  fun_prop

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