continuous_reflTransSymmAux — Mathlib

English

The auxiliary function always lands inside the unit interval.

Русский

Дополнительная функция всегда попадает в единичный интервал.

LaTeX

$$$ transReflReparamAux(I) \in I $$$

Lean4

@[continuity, fun_prop]
theorem continuous_reflTransSymmAux : Continuous reflTransSymmAux :=
  by
  refine continuous_if_le ?_ ?_ (Continuous.continuousOn ?_) (Continuous.continuousOn ?_) ?_
  · fun_prop
  · fun_prop
  · fun_prop
  · fun_prop
  intro x hx
  norm_num [hx, mul_assoc]

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