exact continuous_id.rpow_const fun _ ↦ Or.inr <| div_nonneg (by norm_num) εpos.le
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
Ψ : ℝ → ℝ
ε : ℝ
εpos : 0 < ε
diffΨ : ContDiff ℝ 1 Ψ
⊢ Continuous fun x => x ^ (1 / ε)
no goals