continuous_transReflReparamAux — Mathlib

English

The map transReflReparamAux is continuous on the unit interval.

Русский

Однозначное отображение transReflReparamAux непрерывно на единичном интервале.

LaTeX

$$$\text{continuous}(transReflReparamAux)$$$

Lean4

@[continuity, fun_prop]
theorem continuous_transReflReparamAux : Continuous transReflReparamAux :=
  by
  refine continuous_if_le ?_ ?_ (Continuous.continuousOn ?_) (Continuous.continuousOn ?_) ?_ <;> [fun_prop; fun_prop;
    fun_prop; fun_prop; skip]
  intro x hx
  simp [hx]

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