continuous_transAssocReparamAux — Mathlib

English

The auxiliary reparameterization function transAssocReparamAux is continuous.

Русский

Вспомогательная функция переparamеризаций transAssocReparamAux непрерывна.

LaTeX

$$$$\\operatorname{Continuous}(\\mathrm{transAssocReparamAux}).$$$$

Lean4

@[continuity, fun_prop]
theorem continuous_transAssocReparamAux : Continuous transAssocReparamAux := by
  refine
        continuous_if_le ?_ ?_ (Continuous.continuousOn ?_)
          (continuous_if_le ?_ ?_ (Continuous.continuousOn ?_) (Continuous.continuousOn ?_) ?_).continuousOn ?_ <;>
      [fun_prop; fun_prop; fun_prop; fun_prop; fun_prop; fun_prop; fun_prop; skip; skip] <;>
    · intro x hx
      norm_num [hx]

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