continuous_fromLoop — Mathlib

English

The map fromLoop is continuous for fixed i.

Русский

Карта fromLoop непрерывна при фиксированном i.

LaTeX

$$$\\text{continuous\_fromLoop}(i): \\text{Continuous}$$$

Lean4

theorem continuous_fromLoop (i : N) : Continuous (@fromLoop N X _ x _ i) :=
  ((ContinuousMap.continuous_precomp _).comp <|
        ContinuousMap.continuous_uncurry.comp <|
          (ContinuousMap.continuous_postcomp _).comp continuous_induced_dom).subtype_mk
    _

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