continuous_toLoop — Mathlib

English

The map toLoop, which converts a generalized loop into a loop over a reduced index set, is continuous in i.

Русский

Отображение toLoop, переходящее от обобщённой петли к петле над уменьшенным множеством индексов, непрерывно по i.

LaTeX

$$$\\text{continuous\_toLoop}(i):\\;\\text{Continuous}$$$

Lean4

theorem continuous_toLoop (i : N) : Continuous (@toLoop N X _ x _ i) :=
  Path.continuous_uncurry_iff.1 <|
    Continuous.subtype_mk
      (continuous_eval.comp <|
        Continuous.prodMap
          (ContinuousMap.continuous_curry.comp <| (ContinuousMap.continuous_precomp _).comp continuous_subtype_val)
          continuous_id)
      _

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